| 研究課題/領域番号 |
24220001
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
荒木 啓二郎 九州大学, システム情報科学研究科(研究院, 教授 (40117057)
|
|---|
| 研究分担者 |
大森 洋一 九州大学, システム情報科学研究科(研究院, 助教 (20309727)
山本 修一郎 名古屋大学, 学内共同利用施設等, 教授 (20523294)
片山 徹郎 宮崎大学, 工学部, 准教授 (50283932)
持尾 弘司 筑紫女学園大学, 人間科学部, 准教授 (60331013)
日下部 茂 九州大学, システム情報科学研究科(研究院, 准教授 (70234416)
張 漢明 南山大学, 理工学部, 准教授 (90329756)
|
|---|
| 研究期間 (年度) |
2012-05-31 – 2017-03-31
|
| キーワード | ソフトウェア工学 / 高信頼安全安心システム / 高適用性形式手法 / アーキテクチャ指向モデル化 / ソフトウェアライフサイクル / モデル化支援ツール |
|---|
| 研究実績の概要 |
2015年度は、従来に引き続き、具体例を対象としてシステムの厳密な記述を行い、システムモデル構築のための具体的方法の事例として公開した。その際に、対象システムの本質的な機能と構成を抽象的に記述するのみならず、安全性の分析・保証やシステムの動的振舞い解析などのモデル化の目的に応じて、予備形式化 (Preformal) という概念に基づいて、形式的なシステム記述を構築するための系統的な方法を示した。
特に、システムの安全性については、アーキテクチャに基づき保証ケースを作成する手法ならびに、安全性に関して他の非機能要求との対立を緩和する手法を考案した。
本研究成果の実用性という観点から、ソフトウェア開発における要素技術だけでなく、ソフトウェア開発のプロセスに着目した研究を行った。ソフトウェアの適用が、より大規模複雑なシステム領域へと拡大している動向をふまえて、予備形式化の一つの方向性として、システム理論的因果律モデルの適用を検討した。また、テストにおいて形式手法を適用することを目指して、形式仕様記述からデシジョンテーブルの自動生成ツールの試作を行い、その実現可能性と有用性を確認した。
従来から開発してきたツール群の完成度を高めるとともに、それらの活用法を公開した。VDMPad については、開発対象システムの記述と性質の確認において有用な機能を拡張した。開発の上流工程を形式仕様記述の裏付けのもとに支援する三種類のツール LivelyWalkThrough、WeblyWalkThrough、CloudyWalkThrough をまとめて ViennaTalk としてインターネット上で公開した。また、非形式的な記述から形式仕様作成を支援するツール JODTool を形式手法に関する国際的な共同研究プロジェクト Overture の中に組み入れることにより世界に向けて公開した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究課題に掲げたアーキテクチャ指向形式手法に関する概念および方向性に関する認識を研究代表者ならびに研究分担者の間で共有し、ソフトウェアライフサイクルの要所要所で有効な形式手法適用方法を具体的に提示できるようになり、本研究期間の最後の１年間で研究目的を達成する見通しが得られた。
システムとそれに対する操作や実行環境との間の相互作用をモデル化するための基本方針を定めて、その方針の基に、高信頼安全安心システムの実現に関する研究課題と方法について、形式仕様記述の中のシステムの制約条件に基づく具体的な方法について検討している。形式的システムモデル構築において、予備形式化という概念に基づいた系統的方針のもとでの適用性の高い方法を提示できるという見通しが得られた。具体的には、ソフトウェアの開発と運用プロセスにおける関係者の相互作用に着目し、効果的な形式手法の適用についての知見を得た。予備形式化の一つの方向性として、システム理論的因果律モデルを適用する方法論の評価を行った。また、システムの安全性に関して、対象システムのアーキテクチャに基づいて、安全性を検証するために保証ケースと形式手法の統合方法についての見通しを得た。
本研究の成果は、既に web サーバ ( http://aofa.csce.kyushu-u.ac.jp ) 上で一般に公開している。加えて、本研究で開発しているツールのうち、VDM 関連のツール群は ViennaTalk としてまとめて公開している。また、非形式的記述から厳密なシステム記述の構築を支援するためのツール JODTool は英語化を行った上で、形式手法に関する国際共同研究プロジェクト Overture で提供している支援ツールの中に組み入れて世界に向けて公開している。これらのツール類は、既にいくつかの企業などで有効に利用されている。
|
| 今後の研究の推進方策 |
当初からの、形式手法を基盤として、プロセス、アーキテクチャ、プロダクトラインの三つの軸を組み合わせるという基本的な方針に沿って、ソフトウェアライフサイクルの要所要所において有効な形式手法の適用方法を提示する。特に、運用や保守などの段階で、システムの実行環境やユーザの操作を考慮したシステムの機能や振舞いや安全性などの品質特性の分析や検証を支援する方法を提案する。産学連携のもと、具体的な事例研究に基づいて、形式手法の有効な適用方法を、アークテクチャに基づく予備形式化という新たな概念によって、ソフトウェア開発の現場で共有・再利用可能な形で提示する。
具体的には、PSP (Personal Software Process) や ESPR (Embedded System development Process Reference) などのプロセステンプレートに対して、予備形式化としてシステム理論的因果律モデルを適用し、実際の開発運用現場で利用可能で効果的な形式手法導入のガイドラインの提供を目指す。安全性に関しては、対象システムのアーキテクチャに基づいて、安全を検証するために保証ケースと形式手法を組み合わせた手法を具体化する。また、システムの機能に関する厳密な記述と振舞いに関する記述とに基づいて、テストケース生成を支援する手法を提案し、ツールとして具現化する。
これまでに開発してきたツール群の完成度と適用性を高めて公開するとともに、他の関連ツールとの互換性や連携を図って、高品質ソフトウェア開発の品質と効率の向上に寄与することを目指す。
本研究の報告書をとりまとめて公表するとともに、国際会議の開催やツールを含めた研究成果のインターネット上での公開により本研究の成果を広く世界に発信する。
|
