Wiki
Clone wikiCafeOBJ / OSEK / contents / systemservice / introduction
システムサービス
システムサービスは,先に紹介した枠組の上で,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では, 登録されたタスク,イベント,資源,アラームの集合を返す観測が各々宣言されている.
Updated