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

2001 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: "Transformational Object-Relational Database Model in Formal Methods"IPSJ Transactions on Mathematical Modeling and Its Applications. 42・SIG5(TOM4). 71-80 (2001)
• [Publications] ARAKI Keijiro: "Practical Benefit of Formal Methods : Lessons Learnt through Case Studies"Proceedings of the Joint Workshop on Software Engineering. 72-76 (2001)
• [Publications] 荒木 啓二郎: "形式手法入門:形式仕様記述で何をどう書くか"ソフトウェアシンポジウム2001論文集. 21-26 (2001)
• [Publications] ENDO Toru: "Systematic Generation of Statechart from VDM-SL in Multi-Aspect Formal Methods for System Development"Proceedings of the International Symposium on Future Software Technology. 9-14 (2001)
• [Publications] TANAKA Toshiyuki: "A Generic Graph Analysis Tool with Attributed Path Query"Proceedings of the International Symposium on Future Software Technology. 240-245 (2001)