Wiki

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の立ち上げとシャットダウン，及び，アプリケーションモードの獲得の３つのシステムサービスを，上で定めたモジュールを用いて記述する．

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
  }
}