Wiki

アラーム

OSEK OSは，タスクの活性化やイベントの生起と並んで，アラーム発火時にアラームコールバックルーチンの呼出を行う．

アラームに関するモジュールの記述には，まず，アラームの宣言が必要だろう．

#!python

module ALARM
{
  signature
  {
    [ Alarm ]
  }
}

そして，アラームコールバックルーチンをタスク等と同様にして宣言しよう．

#!python

module ALARM-CALLBACK-ROUTINE
{
  imports
  {
    ex(Entity)
  }
  signature
  {
    [ ACR < Entity ]
  }
}

上のモジュールで宣言したソートACRの項が，アラームコールバックルーチンを表す．アラームは，システム生成時にカウンタ，および，タスクかアラームコールバックルーチンに割り当てられる．

#!python

module COUNTER
{
  signature
  {
    [ Counter ]
  }
}

カウンタを上のように宣言しておいて，アラームの割当を次のように宣言する．

#!python
module ALARM-ASSIGNMENT
{
  imports {
    pr(ALARM)
    pr(COUNTER)
    pr(TRANSITION)
  }
  signature {
    op alarm2counter : Alarm -> Counter
    op alarm2Transition : Alarm -> Transition
  }
}

上で宣言した割当では，アラームの割当先をタスクやアラームコールバックルーチンにはせず，単に遷移としている．

アラームは，カウンタの値が規定値に到達した時に発火する．

ここでは，カウンタの値や規定値には触れず，アラームが発火可能かどうかを示す観測を定める．具体的なカウンタの値や規定値についての記述は，システムサービスで紹介する．

#!python

module EXPIRABLE
{
  import
  {
    pr(OBSERVATION2BOOL)
    pr(ALARM)
  }
  signature
  {
    op expirable : Alarm -> Observation2Bool
  }
}

上のモジュールで宣言した演算expirableは，与えられたアラームが発火可能か否かを返す観測である．

#!python

module EXPIRE
{
  imports
  {
    pr(TRANSITION)
    pr(ASSIGNMENT)
    pr(EXPIRABLE)
  }
  signature
  {
    op expire : Alarm -> Transition
    op expired : Alarm -> Transition
  }
  axioms {
    vars C : State
    vars A : Alarm
    cq expirable(A)(C) = true
       if pre(expire(A),C) .
    cq expire(A)(C) = alarm2Transition(A)(expired(A)(C))
       if pre(expire(A),C) .
    eq expirable(A)(expired(A)(C)) = false .
    eq rev(expired(A),expirable(A)) = true .
  }
}

アラームaに対して遷移expire(a)が起こると， aの発火が止まり，aが割り当てられている遷移が発生する．

OSEK OSは，他にもアラームのキャンセルやアラームの状態の獲得等のサービスも提供している．これらのサービスに係る遷移や観測については，システムサービスで記述する．