2006 Fiscal Year Annual Research Report
ソフトウェア開発のモデル化技法とシステム特性干渉解析に関する研究
| Project/Area Number |
16300007
|
|---|
| Research Institution | KYUSHU UNIVERCITY |
|---|
Principal Investigator |
荒木 啓二郎 九州大学, 大学院システム情報科学研究院, 教授 (40117057)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
福田 晃 九州大学, 大学院システム情報科学研究院, 教授 (80165282)
日下部 茂 九州大学, 大学院システム情報科学研究院, 助教授 (70234416)
張 漢明 南山大学, 数理情報学部, 助教授 (90329756)
中西 恒夫 九州大学, 大学院システム情報科学研究院, 助教授 (70311785)
大森 洋一 九州大学, 大学院システム情報科学研究院, 助手 (20309727)
|
|---|
| Keywords | システムモデル構築 / 形式仕様記述 / 組込みソフトウェア / 多面的記述と分析 / 事例研究 / 高信頼性 / 振舞い分析 / アスペクト指向 |
|---|
| Research Abstract |
2006年度は、従来より引き続いて、形式仕様記述言語VDM-SLおよびVDM++を用いて、エレベータ制御システム、非接触ICカード、産業用ロボットなどの組込みソフトウェアを題材として、システムモデルの構築と記述を行った。また、システムモデルの再利用性を高めるために、プロダクトラインソフトウェア工学におけるフィーチャモデルに基づいて、フィーチャ図とフォールトツリーを用いて、既存正常系フィーチャから異常系フィーチャを発見する方法を提案し、併せて、アスペクト指向プログラミングにおいて、アスペクトの干渉問題について分析を行い、アスペクトの干渉が発生する可能性のある箇所を検出する方法を提案した。
抽象度の高い形式仕様記述と人間に理解しやすい図式表現との相互補完によるシステム記述を行うために、UMLとVDMとを併用して、高品質のソフトウェアを開発する手法について検討し、具体事例を用いて抽象的な仕様記述からC++プログラム作成までを一貫して行い、本手法の有効性を確認した。
さらに、システムの動的振舞いを記述し、分析するために、有限状態機械モデルに基づいたシステム記述を行い、モデル検査手法によって、システムの動的振舞いに関する特性を分析および検証した。また、システムの動作を表すPetri-Netにおいて、具体的動作そのものと動作の種別による抽象化した制御との観点から、Petri-Netを構成する遷移およびプレースに新たな属性を導入して、システムの複雑な動作を見通しよく表現する方法を提案した。
|
