2008 Fiscal Year Annual Research Report
コレオグラフィ記述に基づく組込みシステムの高信頼性設計技法
| Project/Area Number |
19500026
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
結縁 祥治 Nagoya University, 大学院・情報科学研究科, 教授 (70230612)
|
|---|
| Keywords | プログラミング言語 / 並行プログラミング / 組み込みシステム / コレオグラフィー記述言語 / 通信プロセス計算 / エンドポイント射影 |
|---|
| Research Abstract |
本年度は、通信指向プログラミングの記述対象となる組込みシステムの振舞いモデルに対して以下の2点について研究を行った。
(1)組込みシステムにおける割込みの振舞いモデル:
通信指向プログラミングの実現において通信の効率的な実現は割込みに基づいている。割込みは通信を実現する基本的な機構であり、時間に依存した周期的な振舞いを行う組み込みシステムでは必ず含まれる。時間に依存した振舞いモデルはAlurの時間オートマトンに基づく。割込みが発生した場合に実行される割込みハンドラを時間オートマトンで表し、割込みの振舞いを解析するための新たなモデルとして"制御オートマトン"を提案した。制御オートマトンに割込み優先度を全順序的に与えると時間オートマトンに変換できることを示した。これは、単純な割込みに対する検証は時間オートマトンの技法を適用することができることを示している。割込みを含むタスクのスケジューリング可能性が時間オートマトンの到達可能性解析に還元できることを示した。
(2)セッション型の実現機構:
通信指向プログラミングで用いるセッション型の型推論をHaskellにおける実現で自動化する方法を示した。従来からの手法では、言語からある程度独立したセッション型の型推論は人手による助けを必要とする。通信ポートを自然数にエンコードすることで、Haskellの型レベルプログラミングでセッション型の型推論が自動的に可能になることを示した。
以上の検討から、組み込みシステムに対する通信指向プログラミングツールについて研究を進める。
|
