2004 Fiscal Year Annual Research Report
ソフトウェア開発のモデル化技法とシステム特性干渉解析に関する研究
| Project/Area Number |
16300007
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
荒木 啓二郎 九州大学, 大学院・システム情報科学研究院, 教授 (40117057)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
福田 晃 九州大学, 大学院・システム情報科学研究院, 教授 (80165282)
日下部 茂 九州大学, 大学院・システム情報科学研究院, 助教授 (70234416)
張 漢明 南山大学, 数理情報学部, 助教授 (90329756)
中西 恒夫 九州大学, 大学院・システム情報科学研究院, 助教授 (70311785)
大森 洋一 九州大学, 大学院・システム情報科学研究院, 助手 (20309727)
|
|---|
| Keywords | システムモデル構築 / 形式仕様記述 / システム特性 / 多面的記述と分析 / モデル検査 / 事例研究 / 高信頼性 / 組込みソフトウェア |
|---|
| Research Abstract |
2004年度は、形式仕様記述言語VDM-SLおよびVDM++を用いて、ネットワーク分散型情報共有機器、エレベータ制御システム、非接触ICカードなどの組込みソフトウェアを題材として、システムモデルの構築と記述を行った。さらに、それらのモデルに関して、システムの機能や安全性などに関するシステム特性の検証ないし確認を抽象度の高い仕様記述レベルで行った。また、これらのシステムは実機や模型の上に実現して、実際に動作することを確認した。
抽象度の高い形式仕様記述と人間に理解しやすい図式表現との相互補完によるシステム記述を行うために、UMLとVDMとを併用して、システムの機能に着目した記述とシステムの構成に着目した記述との多面的なシステム記述に基づくシステム開発を進める方法について検討して、上記のエレベータ制御システムを具体対象として事例研究を行った。
さらに、上述のシステムの機能や構成の他に、システムの動的振舞いを記述し、分析するために、有限状態機械モデルに基づいたシステム記述を行い、モデル検査手法によって、システムの動的振舞いに関する特性を分析および検証した。VDMによるシステム記述から有限状態機械モデルを導出する手法について検討し、上述の具体システムを対象として、事例研究を行い、多面的記述と分析に関する方法を提示するための基礎的研究を行った。また、Colored Petri-Netによるシステム記述と分析に関する調査研究も行い、多面的なシステム記述と分析に関する方法を提示するための準備を整えている。
|
