Simulation with Interrupts Multitasking call. ret High (AtST S call ret LOW(AOD >>>00 RQ Use invariant“to Interrupt handler specify non- deterministic interference Another taskSimulation with Interrupts & Multitasking call ret Low (A[O]): call, ret High (A[S]): e e Interrupt handler: Another task: IRQ iret switch switch   Use invariant “I” to specify non￾deterministic interference S O