形式的オブジェクト指向方法論に基づく組み込みソフトウェアの構成法の研究

2001 Fiscal Year Annual Research Report

• Project/Area Number: 12480071
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 片山 卓也 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70016468)
• Co-Investigator(Kenkyū-buntansha): 青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (20313702) ; CHERIF Adel 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (10303322)
• Keywords: オブジェクト指向方法論 / 組み込みシステム / 分析モデル / 定理証明 / 並行オブジェクト / スレッド

Research Abstract

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

Research Products

• [Publications] 青木利晃, 立石孝彰, 片山卓也: "定理証明技術のオブジェクト指向分析への適用"コンピュータソフトウェア. 18巻4号. 18-48 (2001)
• [Publications] Toshiaki Aoki, Takaaki Tateishi, Takuya Katayama: "An Axiomatic Formalization of UML Models"Proc. Workshop on Practical UML-based Rigorous Development Methods. 13-28 (2001)
• [Publications] Toshiaki Aoki, Takuya Katayama: "Prototype Execution of Independently Constructed Analysis Models"Automating the Object-Oriented Software Development Methods, ECOOP2001 Workshop. (2001)
• [Publications] Takuya Katayama: "Putting Formalities into Object-Oriented Methodologies"PDCAT(Invited Talk). (2001)