Wiki
Clone wikiCafeOBJ / OSEK / contents / index-e / backup / 20_Systemservices / 3_Interrupt_Handling
Interrupt handling
Observations
os-interrupt:
#!python module OS-INTERRUPT { imports { pr(ISR) } signature { op isOSInterrupt : ISR -> Bool } }
isr-state:
#!python module ISR-AVAILABLE { imports { ex(OBSERVATION2BOOL) } signature { op isrAvailable : -> Observation2Bool } }
isr-disabled:
#!python module ISR-DISABLED { imports { ex(OBSERVATION2BOOL) } signature { op isrDisabled : -> Observation2Bool } }
#!python module ISR-SUSPENDED { imports { ex(OBSERVATION2BOOL) } signature { op isrSuspended : -> Observation2Bool } }
os-isr-available;
#!python module OS-ISR-AVAILABLE { imports { ex(OBSERVATION2BOOL) } signature { op OSisrAvailable : -> Observation2Bool } }
#!python module OS-ISR-DISABLED { imports { ex(OBSERVATION2BOOL) } signature { op OSisrDisabled : -> Observation2Bool } }
#!python module OS-ISR-SUSPENDED { imports { ex(OBSERVATION2BOOL) } signature { op OSisrSuspended : -> Observation2Bool } }
executing
#!python module EXECUTING { imports { ex(OBSERVATION2BOOL) pr(CURRENT) pr(ISR) } signature { op executing : ISR -> Observation2Bool } axioms { vars C : State vars I : ISR eq executing(I)(C) = I == current(C) . } }
pending
#!python module PENDING { imports { ex(EXECUTING) } signature { op pending : ISR -> Observation2Bool } axioms { vars C : State vars I : ISR eq pending(I)(C) = I @ active(C) and not(executing(I)(C)) . } }
State transitions
disable-all:
#!python module DISABLE-ALL { imports { ex(TRANSITION) pr(ISR-AVAILABLE) pr(ISR-DISABLED) pr(OS-ISR-AVAILABLE) pr(OS-ISR-DISABLED) } signature { op disableAll : -> Action } axioms { vars C : State cq isrAvailable(C) = true if pre(disableAll,C) . cq OSisrAvailable(C) = true if pre(disableAll,C) . eq isrAvailable,disableAll(C)) = false . eq OSisrAvailable,disableAll(C)) = false . eq isrDisabled,disableAll(C)) = true . eq OSisrDisabled,disableAll(C)) = true . eq rev(isrAvailable,disableAll) = true . eq rev(OSisrAvailable,disableAll) = true . eq rev(isrDisabled,disableAll) = true . eq rev(OSisrDisabled,disableAll) = true . } }
enable-all:
#!python module ENABLE-ALL { imports { ex(TRANSITION) pr(ISR-AVAILABLE) pr(ISR-DISABLED) pr(OS-ISR-AVAILABLE) pr(OS-ISR-DISABLED) } signature { op enableAll : -> Action } axioms { vars C : State cq isrDisabled(C) = true if pre(enableAll,C) . cq OSisrDisabled(C) = true if pre(enableAll,C) . eq isrAvailable,enableAll(C)) = true . eq OSisrAvailable,enableAll(C)) = true . eq isrDisabled,enableAll(C)) = false . eq OSisrDisabled,enableAll(C)) = false . eq rev(isrAvailable,enableAll) = true . eq rev(isrDisabled,enableAll) = true . eq rev(OSisrAvailable,enableAll) = true . eq rev(OSisrDisabled,enableAll) = true . } }
resume-all
#!python module RESUME-ALL { imports { ex(TRANSITION) pr(ISR-AVAILABLE) pr(ISR-SUSPENDED) pr(OS-ISR-AVAILABLE) pr(OS-ISR-SUSPENDED) } signature { op resumeAll : -> Action } axioms { vars C : State cq isrSuspended(C) = true if pre(resumeAll(C) . cq OSisrSuspended(C) = true if pre(resumeAll(C) . eq isrAvailable,resumeAll(C)) = true . eq OSisrAvailable,resumeAll(C)) = true . eq isrSuspended,resumeAll(C)) = false . eq OSisrSuspended,resumeAll(C)) = false . eq rev(isrAvailable,resumeAll) = true . eq rev(OSisrAvailable,resumeAll) = true . eq rev(isrSuspended,resumeAll) = true . eq rev(OSisrSuspended,resumeAll) = true . } }
resume-os
#!python module RESUME-OS { imports { ex(TRANSITION) pr(OS-ISR-AVAILABLE) pr(OS-ISR-SUSPENDED) } signature { op resumeOS : -> Action } axioms { vars C : State cq OSisrSuspended(C) = true if pre(resumeOS(C) . eq OSisrAvailable,resumeOS(C)) = true . eq OSisrSuspended,resumeOS(C)) = false . eq rev(OSisrAvailable,resumeOS) = true . eq rev(OSisrSuspended,resumeOS) = true . } }
suspend-all
#!python module SUSPEND-ALL { imports { ex(TRANSITION) pr(ISR-AVAILABLE) pr(ISR-SUSPENDED) pr(OS-ISR-AVAILABLE) pr(OS-ISR-SUSPENDED) } signature { op suspendAll : -> Action } axioms { vars C : State cq isrAvailable(C) = true if pre(suspendAll(C) . cq OSisrAvailable(C) = true if pre(suspendAll(C) . eq isrAvailable,suspendAll(C)) = false . eq isrSuspended,suspendAll(C)) = true . eq OSisrAvailable,suspendAll(C)) = false . eq OSisrSuspended,suspendAll(C)) = true . eq rev(isrAvailable,suspendAll) = true . eq rev(isrSuspended,suspendAll) = true . eq rev(OSisrAvailable,suspendAll) = true . eq rev(OSisrSuspended,suspendAll) = true . } }
suspend-os
#!python module SUSPEND-OS { imports { pr(COMPLEMENT) ex(TRANSITION) pr(OS-ISR-AVAILABLE) pr(OS-ISR-SUSPENDED) } signature { op suspendOS : -> Action } axioms { vars C : State cq OSisrAvailable(C) = true if pre(suspendOS(C) . eq OSisrAvailable,suspendOS(C)) = false . eq OSisrSuspended,suspendOS(C)) = true . eq rev(OSisrAvailable,suspendOS) = true . eq rev(OSisrSuspended,suspendOS) = true . } }
cause
#!python module CAUSE { imports { ex(ENABLE) pr(ISR-AVAILABLE) pr(OS-ISR-AVAILABLE) pr(OS-INTERRUPT) } signature { op cause : ISR -> Enable } axioms { vars C : State vars I : ISR cq I @ inactive(C) = true if pre(cause(I)(C) . cq isOSInterrupt(I) = false if pre(cause(I)(C) . cq isrAvailable(C) = true if pre(cause(I)(C) . cq I @ inactive(C) = true if pre(cause(I)(C) . cq isOSInterrupt(I) = true if pre(cause(I)(C) . cq OSisrAvailable(C) = true if pre(cause(I)(C) . } }
finish
#!python module FINISH { imports { ex(DISABLE) pr(ISR) } signature { op finish : ISR -> Disable } axioms { vars C : State vars I : ISR eq sub(finish(I)) = I . cq I @ active(C) = true if pre(finish(I),C)) . } }
System services
enable-all-interrupts
#!python module ENABLE-ALL-INTERRUPTS { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(ENABLE-ALL) pr(CURRENT) pr(ISR) pr(TASK) } signature { op EnableAllInterrupts : -> SystemService } axioms { vars C : System cq pre(enableAll(state(C)) = true if pre(EnableAllInterrupts(C) . cq (isISR(current(state(C))) or isTask(current(state(C)))) = true if pre(EnableAllInterrupts(C) . cq state(EnableAllInterrupts(C)) = enableAll(state(C)) if pre(EnableAllInterrupts(C) . } }
disable-all-interrupts
#!python module DISABLE-ALL-INTERRUPTS { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(DISABLE-ALL) pr(CURRENT) pr(ISR) pr(TASK) } signature { op DisableAllInterrupts : -> SystemService } axioms { vars C : System cq pre(disableAll(state(C)) = true if pre(DisableAllInterrupts(C) . cq (isISR(current(state(C))) or isTask(current(state(C)))) = true if pre(DisableAllInterrupts(C) . cq state(DisableAllInterrupts(C)) = disableAll(state(C)) if pre(DisableAllInterrupts(C) . } }
resume-all-interrupts
#!python module RESUME-ALL-INTERRUPTS { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(RESUME-ALL) pr(CURRENT) pr(ISR) pr(TASK) } signature { op ResumeAllInterrupts : -> SystemService } axioms { vars C : System cq pre(resumeAll(state(C)) = true if pre(ResumeAllInterrupts(C) . cq (isISR(current(state(C))) or isTask(current(state(C)))) = true if pre(ResumeAllInterrupts(C) . cq state(ResumeAllInterrupts(C)) = resumeAll(state(C)) if pre(ResumeAllInterrupts(C) . } }
suspend-all-interrupts
#!python module SUSPEND-ALL-INTERRUPTS { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(SUSPEND-ALL) pr(CURRENT) pr(ISR) pr(TASK) } signature { op SuspendAllInterrupts : -> SystemService } axioms { vars C : System cq pre(suspendAll(state(C)) = true if pre(SuspendAllInterrupts(C) . cq (isISR(current(state(C))) or isTask(current(state(C)))) = true if pre(SuspendAllInterrupts(C) . cq state(SuspendAllInterrupts(C)) = suspendAll(state(C)) if pre(SuspendAllInterrupts(C) . } }
resume-os-interrupts
#!python module RESUME-OS-INTERRUPTS { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(RESUME-OS) pr(CURRENT) pr(ISR) pr(TASK) } signature { op ResumeOSInterrupts : -> SystemService } axioms { vars C : System cq pre(resumeOS(state(C)) = true if pre(ResumeOSInterrupts(C) . cq (isISR(current(state(C))) or isTask(current(state(C)))) = true if pre(ResumeOSInterrupts(C) . cq state(ResumeOSInterrupts(C)) = resumeOS(state(C)) if pre(ResumeOSInterrupts(C) . } }
suspend-os-interrupts
#!python module SUSPEND-OS-INTERRUPTS { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(SUSPEND-OS) pr(CURRENT) pr(ISR) pr(TASK) } signature { op SuspendOSInterrupts : -> SystemService } axioms { vars C : System cq pre(suspendOS(state(C)) = true if pre(SuspendOSInterrupts(C) . cq (isISR(current(state(C))) or isTask(current(state(C)))) = true if pre(SuspendOSInterrupts(C) . cq state(SuspendOSInterrupts(C)) = suspendOS(state(C)) if pre(SuspendOSInterrupts(C) . } }
Updated