Wiki

Clone wiki

CafeOBJ / 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