2014 Fiscal Year Annual Research Report
アーキテクチャ指向形式手法に基づく高品質ソフトウェア開発法の提案と実用化
| Project/Area Number |
24220001
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
荒木 啓二郎 九州大学, システム情報科学研究科(研究院, 教授 (40117057)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 修一郎 名古屋大学, 情報連携統括本部, 教授 (20523294)
張 漢明 南山大学, 理工学部, 准教授 (90329756)
日下部 茂 九州大学, システム情報科学研究科(研究院, 准教授 (70234416)
片山 徹郎 宮崎大学, 工学教育研究部, 准教授 (50283932)
持尾 弘司 筑紫女学園大学, 人間科学部, 准教授 (60331013)
大森 洋一 九州大学, システム情報科学研究科(研究院, 助教 (20309727)
|
|---|
| Project Period (FY) |
2012-05-31 – 2017-03-31
|
| Keywords | ソフトウェア工学 / 高信頼安全安心システム / 高適用性形式手法 / アーキテクチャ指向モデル化 / ソフトウェアライフサイクル |
|---|
| Outline of Annual Research Achievements |
2014年度は、数学的背景を持つ厳密に記述された形式的なシステムモデルの有用性がより明確になったものの、形式的システムモデルの構築法を修得することは容易ではないことが形式手法の導入に対する障壁の一つとなっていることも改めて認識できた。これを改善するために、Preformal (本研究では、予備形式化と呼ぶ) という概念に基づいて、非形式的なアイデアや記述物から出発して形式的システムモデルを構成する手順を系統的に提示できるという見通しを得た。
ソフトウェア開発における品質や効率の向上には要素技術だけでなく、それらを効果的に取入れるソフトウェア開発プロセスが重要であるために、要素技術としての形式手法の導入とプロセス改善とに関する研究を進めた。形式手法導入の阻害要因の一つである実際の開発に形式手法を導入する際に必要な開発プロセスのテーラリングに関して、プロセス改善のモデルに基づいた検討を行った。
実用性の観点から、従来よりテストにおける形式手法の適用について研究を行っている。2014年度は、例外テストケースをシステムアーキテクチャに基づいて系統的に抽出して、十分な例外テストケースを適切に選択する手法を考案した。また、システムの安全性に関して D-Case に基づくシステムの分析や設計を行うことによって、アーキテクチャ指向の形式的システムモデル化を行う際の有効な指針を得た。
公開済みのツール VDMPad の機能を拡張して有用性を高めるとともに、開発の上流工程でアイデアの提示やブレーンストーミングやレビューなどを、形式仕様記述の裏付けのもとに支援する CloudlyWalkThrough ほか２種類のツールをインターネット上で公開した。また、形式仕様作成を支援する用語辞書に関するツールの機能の追加と拡張を行い、複数の学外組織に提供して、その利用技術の確立と有用性の評価を行っている。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究代表者ならびに研究分担者のそれぞれが、各自の研究課題に対して研究を進展させていることに加えて、本研究課題に掲げたアーキテクチャ指向形式手法に関する概念および方向性に関する認識を共有でき、本研究期間の残り２年間で本研究の目的を達成する見通しが得られた。ソフトウェアライフサイクルの各段階で有用な形式手法の適用方法の提案を産学連携のもとに推進中である。
また、システムとそれに対する操作や実行環境との間の相互作用をモデル化するための基本方針を定めて、その方針の基に、高信頼安全安心システムの実現に関する研究課題と方法について、形式仕様記述の中のシステムの制約条件に基づく具体的な方法について検討を開始した。形式的システムモデル構築において、予備形式化という概念に基づいた系統的方法を提示できるという見通しが得られた。
形式的システムモデル構築を支援するツール群については、用語辞書に関するツールと VDMPad の二つは、すでに利用に供している。今後、これらの完成度と実用性を適宜高めていく。他のツールについても完成度と実用性を高めていくとともに、ツール間の連携方法を提示する予定である。
また、大規模複雑システムの効率的な開発で有効なソフトウェアの再利用やオープンソースソフトウェアの利用において、安全性や信頼性の確保を行うための、システム構成ルールを、形式的システムモデルの中に現れるシステムの制約条件に基づいて規定する方法を検討中である。
本研究の成果は、既に公開している web サーバ ( http://aofa.csce.kyushu-u.ac.jp ) 上で一般に公開している。今後は、随時内容を充実させながら、成果の公開を継続していく。
|
| Strategy for Future Research Activity |
アーキテクチャ指向の概念に基づいて、ソフトウェアライフサイクル全般において有効な形式手法の適用方法を提示する。特に、運用や保守などの段階で、システムの実行環境やユーザの操作を考慮したシステムの機能および安全性などの品質特性の分析や検証を支援する方法を提案する。システム開発の当初の意図や想定を明記し管理することによって、大規模システムにおける構成要素間の適合性や派生開発における品質特性の分析・検証を行う方法を考案する。D-Case に基づいてシステムの分析を行うことにより、アーキテクチャ指向でのシステムモデル化の基本的方法を提示する。また、大規模複雑システムの開発において、既存のソフトウェアの再利用やオープンソースソフトウェアの利用の際に、安全性や信頼性の保証を行うための、システム構成ルールを、形式的システムモデルの中で記述するシステムの制約条件に基づいて規定する方法の提案を目指す。
非形式的なアイデアや記述物から形式的システムモデルを構築する際に、予備形式化という概念に基づいた系統的な方法を提案する。その方法に基づいて、現在開発中のツール群の適用性を高めるとともに、それらの連携方法を提示し、JAXA や民間企業との連携のもとに、これらのツールを活用した形式手法適用事例研究を行い、その成果を蓄積して公開し、経験と知見の共有と再利用のための環境を整備する。
ソフトウェア開発の現場で品質保証に実用的な役割を果たしているテストとの関連で、仕様レベル、実装レベルおよびそれらの間をつなぐ抽象化・詳細化における形式手法との連携を、開発プロセスおよびテストプロセスのプラクティスや作業成果物と関連付けながら示す。2014年度に試作した、形式仕様記述からテストで用いるデシジョンテーブルを生成するツール VDTable の適用範囲を広げることで、実用レベルのツールへと発展させる。
|
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] Verifying Curve25519 Software2014
Author(s)
Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, Shang-Yi Yang
Organizer
ACM SIGSAC Conference on Computer and Communications Security
Place of Presentation
米国 アリゾナ
Year and Date
2014-11-04
-
-
-
-
-
-
-
-
-
-
-
-
-
