Wiki
Clone wikiCafeOBJ / OSEK / contents / index-e / backup / 20_Systemservices / 7_Operating_System_Execution_Control
Operating system execution control
Observations
Observation of application mode:
#!python module APPLICATION-MODE { signature { [ ApplicationMode ] op OSDEFAULTAPPMODE : -> ApplicationMode } }
Observation of application mode when the OS starts
#!python module SHOW { imports { ex(OBSERVATION2MODE) } signature { op show : -> Observation2Mode } }
Transitions
Transition at OS start up.
#!python module STARTUP { imports { pr(TRANSITION) pr(SHOW) } signature { op startup : ApplicationMode -> Transition } axioms { vars C : State vars M : ApplicationMode eq show(startup(M)(C)) = M . eq rev(show,startup(M)) = true . } }
System services
StartOS:
#!python module START-OS { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(STARTUP) } signature { op startOS : ApplicationMode -> SystemService } axioms { vars C : System vars M : ApplicationMode eq state(startOS(M)(C)) = startup(M)(state(C)) . } }
GetActiveApplicationMode
#!python module GET-ACTIVE-APPMODE { imports { pr(SYSTEM-SERVICE) pr(SHOW) } signature { op getActiveApplicationMode : -> SystemService } axioms { vars C : System eq state(getActiveApplicationMode(C)) = state(C) . eq show(result(getActiveApplicationMode(C))) = show(state(C)) . } }
ShutdownOS:
#!python module SHUTDOWN-OS { imports { ex(SYSTEM-SERVICE) } signature { op shutdownOS : -> SystemService } }
Updated