研究課題/領域番号 |
12680354
|
研究機関 | 九州大学 |
研究代表者 |
荒木 啓二郎 九州大学, 大学院・システム情報科学研究院, 教授 (40117057)
|
研究分担者 |
持尾 弘司 筑紫女学園大学, 文学部, 講師 (60331013)
張 漢明 南山大学, 数理情報学部, 講師 (90329756)
|
キーワード | 形式仕様記述 / ドメインモデル構築 / 形式手法 / ステートチャート / システム動作記述 / 形式仕様の検査 / システム記述事例研究 / 図式分析ツール |
研究概要 |
本年度は、組込み制御システムの例として、自動販売機を取り上げて、そのモデル構築と形式仕様記述を行った。まず、自動販売機に関する基本的な抽象モデルを構築し、これをより複雑で高度な機能を持たせるよう進化発展させる方法を示した。 次に、日本語で書かれた実際の自動販売機の取扱い説明書を基に、システムの機能の形式的記述とシステムの動作の記述とを行った。機能の記述には、形式仕様記述言語ZとVDM-SL(Vienna Development Method-Specification Language)の2種類を用いた。動作の記述には、ステートチャートを用いた。機能と動作という異なる側面からの記述が、互いに一貫性を持ち、かつ、相互に補完して、対象システムの適切な記述を得る方法を検討した。その方法においては、機能に関する形式仕様記述から系統的な方法によって生成したステートチャートを媒介として、機能の記述と動作の記述との対応付けを行う。これにより、曖昧で不十分なシステム記述から、高品質のシステムモデルならびに形式仕様記述を作成するための系統的かつ効率的方法に対する見通しを得た。 また、昨年度に引続き開発を行った汎用図式表現分析ツールを種々の問題に適用して、その有用性を確認した。この適用経験に基づいて、本ツールの拡張について検討した。特に、ステートチャートを対象として、システムの動作に関する分析を可能とする場合の問題点について考察し、ツールの拡張方針およびその方法に関して具体化を行った。
|