2002 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)
ADEL Cherif 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (10303322)
|
|---|
| Keywords | オブジェクト指向方法論 / 組込みシステム / 分析モデル / 形式的方法論 / 定理証明システム / 並行正規表現 / スレッド / 並行オブジェクト |
|---|
| Research Abstract |
オブジェクト指向方法論は、ビジネスシステムに対しては、最も有効な開発方法論であると認められており,組み込みシステムに対しても要求分析段階での有用性や発展性における優位性は十分に予想されているが、実装に関しては困難な問題もあり適用されていないのが現状である。我々は、(1)形式的オブジェクト指向分析モデルの構築とその上での定理証明技術にもとづく仕様検証、(2)並行オブジェクト構造からスレッド構造への自動的変換、(3)スレッド構造への実時間情報の付与と実時間OSタスク構造の生成、という方法により、オブジェクト指向方法論を適用した組み込みソフトウェアの構成法の研究を行った.以下に,得られた主要な成果を述べる.
(1)形式的オブジェクト指向モデルの構築と検証
組み込みシステムのオブジェクト分析モデルを構築し,モデルの正しさや適切さを検証するために,UMLを構築・検証するための理論体系と構築・検証環境のプロトタイプを構成した.環境は,構築したUMLをテスト実行するシステムと,クラスモデルにつけられた不変表明が満たされることをステートチャートモデルに関する帰納法で証明する検証システムからなる.テスト実行システムでは,MLによる動作記述が,また,検証システムでは定理証明システムHOLが用いられた.
(2)並列オブジェクト構造と並列スレッド構造の変換
並行オブジェクトと並行スレッドの振る舞いを表現できる形式的体系として並行正規表現を考え,並行正規表現間の等価性を判定するための公理体系を与えた.これにより,分析モデルとしの並行オブジェクト表現を,設計モデルとしての並行スレッド表現に等価変換するための基礎が確立した.この公理系にもとづいて,実際に等価変換を行うためにシステムを構築し,具体的な問題に適用して,その有効性を確認することが出来た.今後に残された課題は,この公理系に実時間情報や資源情報を加えて,最適な設計モデルの導出に関する研究に展開することである.
|
Research Products
(7 results)
-
[Publications] 青木利晃, 立石孝彰, 片山卓也: "定理証明技術のオブジェクト指向分析への適用"日本ソフトウェア科学会学会誌コンピュータソフトウェア. 18巻4号. 18-47 (2001)
-
[Publications] Toshiaki Aoki, Takuya Katayama: "Prototype Execution of Independently Constructed Object-Oriented Analysis Model"Automating the Object-Oriented Software Development Methods, OECOOP2001 Workshop. 25-33 (2001)
-
[Publications] Toshiaki Aoki, Takaaki Tateish, Takuya Katayama: "An Axiomatic Formalization of UML Models"Proc. Workshop on Practical UML-Based Rigorous Development Methods. 13-28 (2001)
-
[Publications] Mitsutaka Okazaki, Toshiaki Aoki, Takuya Katayama: "Extracting Threads from Concurrent Objects for the Design of Embedded Systems"Proc. Asia-Pacific Software Engineering Conference APSEC2002. 107-116 (2002)
-
[Publications] Takaaki Tateishi, Toshiaki Aok, Takuya Katayama: "Successive Behavior Approximation Method for Verifying Distributed Objects"Proc. Third International Conference on Parallel and Distributed Computing, Application and Technologies. 439-446 (2002)
-
[Publications] 立石孝彰, 青木利晃, 片山卓也: "振舞い近似手法を用いたステートチャートに対する不変性の検証"情報処理学会論文誌「オブジェクト指向技術特集」. 44巻6号. (2003)
-
[Publications] Mitsutaka Okazaki, Toshiaki Aoki, Takuya Katayama: "Formalizing Sequence Diagrams and State Machines Using Concurrent Regular Expression"Proc. Second International Workshop on Scenarios and State Machines : Models, Algorithms and Tools, ICSE2003 Workshop. 74-79 (2003)
