Wiki

システムサービス

システムサービスは，先に紹介した枠組の上で，Interfaceの部分ソートとして宣言できる．まず，割込処理等も含めて現在システムで実行されている処理単位を返す観測を次のように定める．

#!python


module CURRENT
{
  imports
  {
    pr(OBSERVATION2ENTITIES)
  }
  signature
  {
    op current : -> Observation2Entities
  }
}

システムサービスは，次のように記述できる．

#!python

module SYSTEM-SERVICE
{
  imports
  {
    ex(INTERFACE)
    pr(CURRENT)
  }
  signature
  {
    [ SystemService < Interface ]
    op available : Entity SystemService System -> Bool
  }
  axioms
  {
    vars F : SystemService
    vars S : System
    vars X : Entity
    cq available(X,F,S) = true
       if pre(F,S) and (X @ current(state(S))) .
  }
}

システムサービスの使用の可否

自身の種類に応じて，処理単位が使用できるシステムサービスがOSEK/VDX仕様で定められている availableは，与えられた処理単位が指定されたシステムサービスを使用できるか否かを返す．システムサービスが正しく実行されるには，そのシステムサービスを現在システムで実行中の処理単位が使用可能でなければならない．

処理単位が使用できるシステムサービスの一覧は，CafeOBJでは以下のように記述できる．

#!python

    vars T : Task
    vars I1 : ISR1
    vars I2 : ISR2
    vars EH : ErrorHook
    vars PrH : PreTaskHook
    vars PoH : PostTaskHook
    vars SUH : StartupHook
    vars SDH : ShutdownHook
    vars ACR : AlarmCallback
    vars S : System

    eq available(T,ActivateTask,S) = true .
    eq available(I2,ActivateTask,S) = true .

    eq available(T,TerminateTask,S) = true .

    eq available(T,ChainTask,S) = true .

    eq available(T,Schedule,S) = true .

    eq available(T,GetTaskID,S) = true .
    eq available(I2,GetTaskID,S) = true .
    eq available(EH,GetTaskID,S) = true .
    eq available(PrH,GetTaskID,S) = true .
    eq available(PoH,GetTaskID,S) = true .

    eq available(T,GetTaskState,S) = true .
    eq available(I2,GetTaskState,S) = true .
    eq available(EH,GetTaskState,S) = true .
    eq available(PrH,GetTaskState,S) = true .
    eq available(PoH,GetTaskState,S) = true .

    eq available(T,DisableAllInterrupts,S) = true .
    eq available(I1,DisableAllInterrupts,S) = true .
    eq available(I2,DisableAllInterrupts,S) = true .

    eq available(T,EnableAllInterrupts,S) = true .
    eq available(I1,EnableAllInterrupts,S) = true .
    eq available(I2,EnableAllInterrupts,S) = true .

    eq available(T,SuspendAllInterrupts,S) = true .
    eq available(I1,SuspendAllInterrupts,S) = true .
    eq available(I2,SuspendAllInterrupts,S) = true .
    eq available(EH,SuspendAllInterrupts,S) = true .
    eq available(PrH,SuspendAllInterrupts,S) = true .
    eq available(PoH,SuspendAllInterrupts,S) = true .
    eq available(ACR,SuspendAllInterrupts,S) = true .

    eq available(T,ResumeAllInterrupts,S) = true .
    eq available(I1,ResumeAllInterrupts,S) = true .
    eq available(I2,ResumeAllInterrupts,S) = true .
    eq available(EH,ResumeAllInterrupts,S) = true .
    eq available(PrH,ResumeAllInterrupts,S) = true .
    eq available(PoH,ResumeAllInterrupts,S) = true .
    eq available(ACR,ResumeAllInterrupts,S) = true .

    eq available(T,SuspendOSInterrupts,S) = true .
    eq available(I1,SuspendOSInterrupts,S) = true .
    eq available(I2,SuspendOSInterrupts,S) = true .

    eq available(T,ResumeOSInterrupts,S) = true .
    eq available(I1,ResumeOSInterrupts,S) = true .
    eq available(I2,ResumeOSInterrupts,S) = true .

    eq available(T,GetResource,S) = true .
    eq available(I2,GetResource,S) = true .

    eq available(T,ReleaseResource,S) = true .
    eq available(I2,ReleaseResource,S) = true .

    eq available(T,SetEvent,S) = true .
    eq available(I2,SetEvent,S) = true .

    eq available(T,ClearEvent,S) = true .

    eq available(T,GetEvent,S) = true .
    eq available(I2,GetEvent,S) = true .
    eq available(EH,GetEvent,S) = true .
    eq available(PrH,GetEvent,S) = true .
    eq available(PoH,GetEvent,S) = true .

    eq available(T,WaitEvent,S) = true .

    eq available(T,GetAlarmBase,S) = true .
    eq available(I2,GetAlarmBase,S) = true .
    eq available(EH,GetAlarmBase,S) = true .
    eq available(PrH,GetAlarmBase,S) = true .
    eq available(PoH,GetAlarmBase,S) = true .

    eq available(T,GetAlarm,S) = true .
    eq available(I2,GetAlarm,S) = true .
    eq available(EH,GetAlarm,S) = true .
    eq available(PrH,GetAlarm,S) = true .
    eq available(PoH,GetAlarm,S) = true .

    eq available(T,SetRelAlarm,S) = true .
    eq available(I2,SetRelAlarm,S) = true .

    eq available(T,SetAbsAlarm,S) = true .
    eq available(I2,SetAbsAlarm,S) = true .

    eq available(T,CancelAlarm,S) = true .
    eq available(I2,CancelAlarm,S) = true .

    eq available(T,GetActiveApplicationMode,S) = true .
    eq available(I2,GetActiveApplicationMode,S) = true .
    eq available(EH,GetActiveApplicationMode,S) = true .
    eq available(PrH,GetActiveApplicationMode,S) = true .
    eq available(PoH,GetActiveApplicationMode,S) = true .
    eq available(SUH,GetActiveApplicationMode,S) = true .
    eq available(SDH,GetActiveApplicationMode,S) = true .

    eq available(T,ShutdownOS,S) = true .
    eq available(I2,ShutdownOS,S) = true .
    eq available(EH,ShutdownOS,S) = true .
    eq available(SUH,ShutdownOS,S) = true .

OSへの登録

OSEK OSは，利用者にタスクやイベント等の登録手段を提供している．登録手段全般を表すモジュールを，INTERFACEを拡張して次のように定める．

#!python

module REGISTRATION
{
  imports {
    ex(INTERFACE)
  }
  signature {
    [ Registration < Interface ]
  }
}

これをベースにして，タスクやイベントなどの要素の登録を次のように記述する．

#!python

module DECLARE
{
  imports {
    ex(TRANSITION)
    ex(DECLARED-TASK)
    ex(DECLARED-EVENT)
    ex(DECLARED-RESOURCE)
    ex(DECLARED-ALARM)
  }
  signature {
    op declare : Task -> Transition
    op declare : Event -> Transition
    op declare : External -> Transition
    op declare : Alarm -> Transition
  }
  axioms {
    vars C : State
    vars T : Task
    vars E : Event
    vars R : External
    vars A : Alarm
    eq declaredTask,declare(T)(C)) = declaredTask(C), T .
    eq declaredEvent,declare(E)(C)) = declaredEvent(C), E .
    eq declaredResource,declare(R)(C)) = declaredResource(C), R .
    eq declaredAlarm,declare(A)(C)) = declaredAlarm(C), A .
    eq depend(declaredTask,declare(T)) = true .
    eq depend(declaredEvent,declare(E)) = true .
    eq depend(declaredResource,declare(R)) = true .
    eq depend(declaredAlarm,declare(A)) = true .
  }
}

ここで，DECLARED-TASK，DECLARED-EVENT，DECLARED-RESOURCE，DECLARED-ALARMでは，登録されたタスク，イベント，資源，アラームの集合を返す観測が各々宣言されている．