Wiki

OSEK OS のアーキテクチャ

ここでは，OSEK OS の処理単位と処理レベルをCafeOBJで記述する．

OSEK OSの処理単位

OSEK OSの処理単位（Entity）には，割込処理ルーチン（Interrupt Service Routine）とタスク（Task）がある．まず，処理単位のソートを次のモジュールENTITYで宣言する．

#!python

module ENTITY
{
  signature
  {
    [ Entity ]
  }
}

割込処理ルーチンとタスクのソートは，各々以下のモジュールで宣言される．

#!python

module ISR
{
  imports {
    ex(ENTITY)
  }
  signature {
    [ ISR < Entity ]
  }
}

割込処理ルーチンのソートISRは，処理単位のソートEntityの部分ソートとして宣言される．

#!python

module TASK
{
  imports {
    ex(ENTITY)
  }
  signature {
    [ Task < Entity ]
  }
}

割込処理ルーチンと同様，タスクのソートTaskもまた，Entityの部分ソートとして宣言される．

また，割込処理ルーチンやタスク以外の処理単位を次のように宣言する．ここではスケジューラ等を想定している．

#!python

module INTERNAL-ACTIVITY
{
  imports {
    ex(ENTITY)
  }
  signature {
    [ InternalActivity < Entity ]
  }
}

処理レベル

OSEKは，３つの処理レベル（Processing Level）を定めている．

割込処理レベル（Interrupt Processing Level）
スケジューラ用の論理レベル（Logical Level）
タスクレベル（Task Level）

OSEKでは，優先度は自然数で表現され，処理レベルは自然数上の区間で表される．自然数上の区間は，NATを拡張して次のように定義できる．

#!python

module INTERVAL
{
  imports
  {
    ex(NAT)
  }
  signature {
    [ Interval ]
    op top : Interval -> Nat
    op bot : Interval -> Nat
    op _@_ : Nat Interval -> Bool
    op # : Interval -> Nat
  }
  axioms
  {
    vars L : Interval
    vars I : Nat
    eq bot(L) <= top(L) = true .
    eq #(L) = top(L) - bot(L) + 1 .
    cq I @ L = true
       if  bot(L) <= I and I <= top(L) .
  }
}

Intervalの項で表現される区間は閉区間である．演算botとtopは，各々区間の最小値と最大値を表している．任意の区間Lに対し，Lの最小値bot(L)と最大値top(L)の間にある自然数は，区間Lに属する．また，#（L）は，区間Lに属する自然数の数を表す．任意の区間Lに対して #（L）＞ 0 となるので，Lは空ではない，

OSEK OSの処理レベルは，自然数上の区間として定義される．

#!python

module PROCESSING-LEVEL
{
  imports
  {
    ex(INTERVAL)
  }
  signature {
    op interruptLevel : -> Interval
    op logicalLevel : -> Interval
    op taskLevel : -> Interval
  }
  axioms
  {
    vars I J : Nat
    cq I > J = true
       if  I @ interruptLevel and J @ logicalLevel .
    cq I > J = true
       if  I @ logicalLevel and J @ taskLevel .
    cq I > J = true
       if  I @ interruptLevel and J @ taskLevel .
  }
}

割込処理レベルの優先度は論理レベルやタスクレベルの優先度よりも高く，論理レベルの優先度はタスクレベルの優先度よりも高い．因みに，自然数上の大小関係＞は推移的なので，上のモジュールで宣言した最後の条件付き棟式は，本来であれば不要である．ただ，CafeOBJ処理系に内蔵されている自然数のモジュールでは，大小関係の推移律は定義されていないので，ここでは記述している．

割込処理ルーチンやタスクには予め優先度が割り当てられている．割込処理ルーチンに割り当てられている優先度は割込処理レベルにあり，タスクに割り当てられている優先度はタスクレベルにある．

#!python

module ASSIGNED-PRIORITY
{
  imports
  {
    ex(PROCESSING-LEVEL)
    pr(ISR)
    pr(TASK)
    pr(INTERNAL-ACTIVITY)
  }
  signature
  {
    op assigned : Entity -> Nat
  }
  axioms
  {
    vars I : ISR
    vars R : InternalActivity
    vars T : Task
    eq assigned(I) @ interruptLevel = true .
    eq assigned(R) @ logicalLevel = true .
    eq assigned(T) @ taskLevel = true .
  }
}