| 研究課題/領域番号 |
14380141
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
阿草 清滋 名古屋大学, 情報科学研究科, 教授 (90026360)
|
|---|
| 研究分担者 |
結縁 祥治 名古屋大学, 情報科学研究科, 助教授 (70230612)
濱口 毅 名古屋大学, 情報科学研究科, 助手 (90273284)
山本 晋一郎 愛知県立大学, 情報科学部, 助教授 (40240098)
|
|---|
| キーワード | 時間オートマトン / リアクティブシステム / コード生成 / ソフトウェア信頼性 / 組み込みシステム |
|---|
| 研究概要 |
本年度はリアクティブシステムの形式モデルをミドルウェアとして応用するためのシステム構築手法およびその基礎理論について研究を行った。
時間オートマトンおよび時間を導入したπ計算を基に信頼性の高いコーディングを形式的モデルの振舞い的性質からある程度機械的に導き出すことによって開発工程を効率化するための手法を示した。
(1)時間付きπ計算の代数的性質に関する検討
並行計算の形式モデルであるπ計算に時間を導入した体系において合同性が成立する条件について検討を行った。ここでは、時間の概念を相互に持つモジュールが単一であれば合同性が保存されることを示した。
(2)時間オートマトンに基づくプログラムコード生成手法
時間オートマトンモデルに基づくUPPAALモデルを介して、設計とコーディングの整合性をチェックしながら時間を含めた状態遷移に関するコーディングを効率化する手法を示した。組み込みシステムをターゲットとして、ロボットAIBOのプログラミング環境およびLego Mindstormのプログラミング環境に対して応用を行い、それぞれの環境で開発が効率化されることを示した。
(3)ミドルウェアとしての時間オートマトンツール
UPPAALが提供するXML記述を動作に対する高抽象度のAPIとみなし、実際のシステムに課される制約を加えることで下位レベルのコードを生成する開発環境について研究を行った。
本研究の結論として得られた知見は、リアクティブシステムに対するミドルウェアによって信頼性の高い並行システムを構成するためには、単に関数の抽象化を行うだけではなく、状態を含めた振る舞いの抽象化を行わなければならないということである。
|
