形式手法に基づく高品質組込み制御システム開発法の系統化に関する基礎的研究

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12680354
• Research Institution: Kyushu University
• Principal Investigator: 荒木 啓二郎 九州大学, 大学院・システム情報科学研究院, 教授 (40117057)
• Co-Investigator(Kenkyū-buntansha): 持尾 弘司 筑紫女学園大学, 文学部, 講師 (60331013) ; 張 漢明 南山大学, 数理情報学部, 講師 (90329756)
• Keywords: 形式仕様記述 / ドメインモデル構築 / 形式手法 / 図式表現 / 図式分析ツール / 形式仕様の検査 / システム記述事例研究 / 段階的詳細化設計

Research Abstract

本年度は、組込みシステムの具体事例として、配電線監視制御システム、自動倉庫システム、自動販売機などのシステムモデル構築ならびに形式仕様記述を行った。形式仕様記述言語としては、ZとVDM-SL(Vienna Development Method-Specification Language)の2種類を使用した。システムモデルの抽象度の違い、ならびに、記述および分析の目的に応じた記述言語の使いわけ、モデル構築などに関して、有用な知見を得た。今後は、これらの事例に関して、より深く記述および分析を進めて、高品質組込みシステムの効率的な開発法を提案することを目指す。
システムモデル構築には図式表現がしばしば使用される。本年度は、図式表現に対する汎用の分析ツールを試作し、上記の事例に適用して、このツールの有効性を示した。汎用の図式分析機能により、各種の応用領域に適した図式表現法、ならびに、それに対する意味付けおよびそれに基づく分析を支援することにより、システムモデル構築ならびに仕様記述を柔軟にかつ効率よく進める基盤を提供することができる。この汎用基盤の上に、上述の開発法を支援するツールの開発を行い、その有用性を実証する。
また、形式仕様に対する検査方法について検討し、上記の具体事例に対して仕様の検査を実施していくつかの不備を発見することができた。これにより得られた仕様の品質保証に関する知見を基に、今後は、高品質システム仕様を効率よく得るための方法と支援ツールに関する研究を進める。

Research Products

• [Publications] Pujianto Yugopuspito: "UML Refinement for Object-Relational Database"Proceedings of the International Symposium on Future Software Technology ISFST-2000. 27-31 (2000)
• [Publications] Keijiro Araki: "Case Studies of Formal Approaches to Domain Modelling and Specification"Proceedings of the International Symposium on Future Software Technology ISFST-2000. 213-218
• [Publications] 田中俊行: "実用規模のシステムへの形式手法の適用事例"ソフトウェア工学の基礎VII. 205-208 (2000)
• [Publications] 張漢明: "グラフ分析エンジンGOAeの開発"ソフトウェア工学の基礎VII. 209-212 (2000)
• [Publications] 丸山博史: "プログラムスライシングのVRMLへの導入とその改良"情報処理学会論文誌:数理モデル化と応用. 41・SIG7(TOM3). 1-11 (2000)