Wiki
Clone wikiCafeOBJ / OSEK / contents / systemservice / os
OS実行制御
ここでは,OSの立ち上げやシャットダウンに係るシステムサービスを記述する.
OSの立ち上げにはアプリケーションモードを与えなければならない. アプリケーションモードは,上のモジュールで宣言される.
#!python module APPLICATION-MODE { signature { [ ApplicationMode ] op OSDEFAULTAPPMODE : -> ApplicationMode } }
ここではディフォルトのモードしか用意していないが, 適宜このモジュールを拡張し,独自のモードを宣言できる.
立ち上げ時のアプリケーションモードは次の観測で見ることができる.
#!python module SHOW { imports { ex(OBSERVATION2MODE) } signature { op show : -> Observation2Mode } }
#!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 . } }
OSの立ち上げとシャットダウン,及び,アプリケーションモードの獲得の3つの システムサービスを,上で定めたモジュールを用いて記述する.
OS立ち上げ
#!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)) . } }
アプリケーションモードの観測
#!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)) . } }
OSのシャットダウン
#!python module SHUTDOWN-OS { imports { ex(SYSTEM-SERVICE) } signature { op shutdownOS : -> SystemService } }
Updated