2014 Fiscal Year Annual Research Report
形式手法の統合によるシームレスなソフトウェア開発手法の提案
| Project/Area Number |
24500035
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | 形式手法 / モデル検査 / 形式仕様記述 / テスト / 車載ソフトウェア |
|---|
| Outline of Annual Research Achievements |
平成26年度(最終年度)は，当初の計画どおり，ツールの実装と，提案手法の評価を行った．実装したツールは，形式仕様記述言語Event-Bによる記述と境界(Bounds)を入力とし，提案したアルゴリズムに基づいて，設計モデルを検査するためのPromela記述を自動的に出力する．出力されたPromela記述と同じくPromelaにより記述された設計モデルを組み合わせ，モデル検査ツールSpinで自動的に検査することにより，仕様と設計の整合性を自動的に検証することができる．また，このツールを，車載オペレーティングシステムの事例に適用し，評価を行った．これにより，提案手法とツールは，境界の設定により状態爆発問題を回避しつつ，十分な誤り検出能力を持つことを示すことができた．
研究期間全体を通しては，おおむね順調に進んだと考えている．当初の予定どおり，複数の形式手法を統合し，ソフトウェア開発の上流工程から下流工程までをシームレスに接続した．さらには，実際の車載オペレーティングシステムの事例に適用し，提案手法の有効性を示すことができた．本研究の意義は，形式手法に基づいて，全行程をカバーすることができたことである．我々が注目している題材の車載オペレーティングシステムでは，開発工程の一部に形式手法を適用し，検証した事例のみであった．一方で，我々は，仕様記述から実装のテストまで，シームレスに接続し，全行程をカバーすることができた．これは，大きな意義のある成果であると言える．また，我々が検証している車載オペレーティングシステムは，実際に世の中で使われているものであり，それを対象として提案手法の有効性を示すことができた．これにより，産業界における形式手法の採用が加速され，ソフトウェアの信頼性，安全性が向上することを期待している．
|
Research Products
(8 results)
