CafeOBJによるOSEK/VDX仕様記述の枠組

OSEK OSのうち，OSEK/VDX仕様で定められる部分は，下のADJ図で示す枠組に従いCafeOBJで記述される．ADJ図に現れる円はソートを，矢印は演算を各々表している．

OSEK/VDX仕様は，内部状態の遷移に関わる諸機能と，それらの機能を踏まえた，OSが提供するシステムサービスについて述べている．上に挙げた枠組は，内部状態遷移記述向けのものと，システムサービス記述向けのものに分けられる．以下，内部状態遷移記述向けの枠組とシステムサービス記述向けの枠組に分けて説明する．

CafeOBJによるOSEK OS 内部状態遷移記述の枠組

下図で示されている濃い実線の部分が，OSEK OS の内部状態遷移を記述するための枠組である．

この枠組を定めるCafeOBJモジュールを順を追って紹介しよう．

モジュールVALUEは，状態を構成する属性の値のソートValueを宣言している．

#!python

module VALUE
{
  signature
  {
    [ Value ]
  }
}

モジュールCONTAINERで宣言されているソートContainerの項は，複数の属性が混在している状況である．

#!python

module CONTAINER
{
  signature
  {
    [ Container ]
  }
}

モジュールOBSERVATIONでは，Containerの項から指定された属性の値を引き出す演算を宣言している．

#!python

module OBSERVATION
{
  imports
  {
    pr(CONTAINER)
    ex(VALUE)
  }
  signature
  {
    [ Observation ]
    op __ : Observation Container -> Value
    op pre : Observation Container -> Bool
  }
}

属性の値を含め，混沌とした状況から何らかの値を引き出す行為は「観測」と呼ばれる．モジュールOBSERVATIONでは，ソートObservationの項が，そのような観測を表している．演算__は，混沌とした状況を表すContainerの項に対する，Observationの項が表す観測の適用であり，演算preは，観測の適用に際して満たされていなければならない事前条件である．以降，必要に応じて，具体的な観測とその値のソートをObservationやValueの部分ソートとして各々宣言し，宣言したソートで観測の適用演算を宣言し直していけばよい．

モジュールSTATEは，OSEK OS の内部状態のソートStateを宣言している．

#!python

module STATE
{
  imports
  {
    ex(CONTAINER)
  }
  signature
  {
    [ State < Container ]
    op init : -> State
  }
}

Stateは，Containerの部分ソートとして宣言される．モジュールCONTAINERで宣言された，観測の適用__や，その事前条件であるpreは，Stateに対しても用いることができる．また，ここで宣言されている項initは，初期状態を表している．

モジュールTRANSITIONは状態遷移を表す．

#!python

module TRANSITION
{
  imports
  {
    ex(STATE)
  }
  signature
  {
    [ Transition ]
    op __  : Transition State -> State
    op pre : Transition State -> Bool
  }
}

ソートTransitionの項は，状態を遷移させる行為を表す．そして，状態を表すソートStateの項に対する遷移の適用を演算__で表している．演算preは，遷移の適用に際して満たされていなければならない事前条件である．以降，必要に応じて，具体的な遷移のソートをTransitionの部分ソートとして宣言していく．

CafeOBJによるOSEK OS システムサービス記述の枠組

CafeOBJによるOSEK OSの内部状態遷移記述の枠組以外の部分，すなわち，下図の濃い実線の部分が，OSEK OS が提供するシステムサービスをCafeOBJで記述するための枠組となる．OSEK/VDX仕様で定められているシステムサービスは,返り値の他に複数の出力引数を持ち,さらに副作用で状態が変化する.この呼出系列をそのままCafeOBJで表現することはできない.そこで,ここでは，システムサービスの呼出をシステム返す演算として宣言し,サービスの呼出後にその返値や出力引数に返される値をシステムから取り出す,という記述方針を採る.

まず，システムサービスの呼出で返されるステータスを次のモジュールで宣言しよう．

#!python

module STATUS
{
  signature
  {
    [ Status ]
  }
}

以降，必要に応じてソートStatusの項として，具体的なステータスを宣言していく．

次に挙げるモジュールRESULTは，システムサービスの呼出の出力引数とそこに返される値を記述するためのものである．

#!python

module RESULT
{
  imports
  {
    ex(CONTAINER)
  }
  signature {
    [ Result < Container ]
  }
}

システムサービスの出力は，ResultというContainerの部分ソートの項で表現される．システムサービスの出力引数に返される値は，出力引数を観測として宣言すれば，観測を呼出結果に適用することで出力引数に返された値を取り出すことができる．

システムは，次のモジュールで定められる．

#!python

module SYSTEM
{
  imports
  {
    ex(STATE)
    ex(STATUS)
    ex(RESULT)
  }
  signature
  {
    [ System ]
    op state : System -> State
    op status : System -> Status
    op result : System -> Result
  }
}

ソートSystemの項がシステムを表す．システムの内部状態，システムサービスが返すステータス，そしてシステムサービスの出力は各々，演算state，status，resultを介してシステムから取り出すことができる．

モジュールINTERFACEは，システムに対する操作の適用を記述するためのものである．

#!python

module INTERFACE
{
  imports
  {
    ex(SYSTEM)
  }
  signature
  {
    [ Interface ]
    op __ : Interface System -> System
    op pre : Interface System -> Bool 
  }
}

ソートInterfaceの項は，システムに適用される操作のインターフェースを表す．そして，システムへの操作の適用は，状態遷移Transitionや観測Observationと同様，演算__で表す．演算preは，操作の適用に際して満たされていなければならない事前条件である．以降，具体的なシステムサービスは，Interfaceの項として宣言していく．