| 研究課題/領域番号 |
16300007
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
荒木 啓二郎 九州大学, 大学院・システム情報科学研究院, 教授 (40117057)
|
|---|
| 研究分担者 |
福田 晃 九州大学, 大学院・システム情報科学研究院, 教授 (80165282)
日下部 茂 九州大学, 大学院・システム情報科学研究院, 助教授 (70234416)
張 漢明 南山大学, 数理情報学部, 助教授 (90329756)
中西 恒夫 九州大学, 大学院・システム情報科学研究院, 助教授 (70311785)
大森 洋一 九州大学, 大学院・システム情報科学研究院, 助手 (20309727)
|
|---|
| キーワード | システムモデル構築 / 形式仕様記述 / 組込みソフトウェア / 多面的記述と分析 / 事例研究 / 高信頼性 / 振舞い分析 / アスペクト志向 |
|---|
| 研究概要 |
2005年度は、形式仕様記述言語VDM-SLおよびVDM++を用いて、エレベータ制御システム、非接触ICカード、産業用ロボットなどの組込みソフトウェアを題材として、システムモデルの構築と記述を行った。さらに、それらのモデルに関して、システムの機能や安全性などに関するシステム特性の検証や確認を抽象度の高い仕様記述レベルで行った。また、プロダクトラインソフトウェア工学におけるフィーチャモデルに基づいて、非機能フィーチャの記述と相互干渉分析の手法について検討した。
抽象度の高い形式仕様記述と人間に理解しやすい図式表現との相互補完によるシステム記述を行うために、UMLとVDMとを併用して、高品質のソフトウェアを開発する手法について検討し、エレベータ模型を具体対象として抽象的な仕様記述からC++プログラム作成までを一貫して行い、本手法の有効性を確認した。
さらに、上述のシステムの機能や構成の他に、システムの動的振舞いを記述し、分析するために、有限状態機械モデルに基づいたシステム記述を行い、モデル検査手法によって、システムの動的振舞いに関する特性を分析および検証した。VDMによるシステム記述から有限状態機械モデルを導出する手法を提案し、ツールを試作した。また、産業用ロボットを具体的題材にして、並行動作プロセス間の相互作用をアスペクトとみなしてCSPに基づいてシステムの動的振舞いを記述し分析する方法について検討した。
|
