Wiki
Clone wikiCafeOBJ / OSEK / contents / architecture
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は,3つの処理レベル(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) . } }
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 . } }
Updated