| 研究課題/領域番号 |
12480071
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
片山 卓也 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70016468)
|
|---|
| 研究分担者 |
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (20313702)
CHERIF Adel 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (10303322)
|
|---|
| キーワード | オブジェクト指向方法論 / 組み込みシステム / 分析モデル / 定理証明 / 並行オブジェクト / スレッド |
|---|
| 研究概要 |
本研究課題では、オブジェクト指向方法論による組み込みシステムの科学的構成法の確立を目指して研究をおこなってきたが、平成13年度は下記研究課題1および研究課題2の研究を行なった。
1.組み込みシステムに特化した形式的オブジェクト指向分析法の展開、定理証明技術およびプロトタイプ実行に基づくモデル検証
2.並行オブジェクト構造からスレッド構造への変換
即ち、形式的オブジェクト指向方法論を用いて組み込みシステムの形式的分析モデルを構成し、その適切さを定理証明系やプロトタイプ実行を通して確立する方法論の研究、および並行オブジェクトで与えられる統合分析モデルを現実の計算機アーキテクチャに適合させ、効率良く実行させるための研究を行なった。
前者に関しては、(1)組み込みシステムのモデル化に必要な分析モデルの形式化と、それらの間の整合性検証法の確立、(2)分析モデルの高階論理シズテムHOLでの公理化、分析モデル間の整合性検証法のための証明システムに関して有効な成果を得た。また、HOLでの証明では、対象ドメインの公理化が必須であることから、どのドメインにも有効なオブジェクトドメインの公理化を行った。
後者に関しては、並行オブジェクトの動作を並行スレッドに変換するための変換規則を得た。これは並行オブジェクトを表現する並行正規表現をスレッド正規表現に変換するもので、変換規則の健全性を証明した。
|
