2013 Fiscal Year Research-status Report
形式手法の統合によるシームレスなソフトウェア開発手法の提案
| Project/Area Number |
24500035
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
|
|---|
| Keywords | 形式手法 / モデル検査 / 形式仕様 |
|---|
| Research Abstract |
本年度は，Event-Bで作成された形式仕様を用いてPromelaで作成された設計モデルを検証する手法を形式的に定義した．Promelaで作成された設計モデルは，モデル検査ツールSPINにより検査される．この際，時相論理や表明などにより，性質を記述する．しかしながら，実践的には，時相論理や表明による仕様の表現は限定的にならざるをえない．そこで，Promelaで作成された設計モデルが，Event-Bで作成された形式仕様を満たしているかどうか検証する手法を提案し，以下の手順で形式的に定義した．
(1)状態遷移システム基づいた形式化：提案した手法では，Event-Bで作成された形式仕様とPromelaで作成された設計モデルの間に模倣関係が存在することを検証する．一方で，Event-BとPromelaでは，記述方式が異なる．そこで，状態遷移システムに基づいて，Event-BとPromelaによる記述を形式的に表現し，それらの間の模倣関係を定義した．
(2) 有界性の定義：Event-Bで作成された形式仕様は，潜在的に，無限の状態を持ち得る．一方で，Promelaによる記述は，有限状態に限られている．そこで，前者を有限状態に限定する境界(Bounds)を定義した．
(3) 環境の生成：(1)と(2)の定義に基づいて，模倣関係を検査するための状態遷移モデルを定義した．この状態遷移モデルのことを環境と呼ぶ．また，Event-Bで作成された形式仕様からPromelaで記述された環境を生成するアルゴリズムを提案した．生成された環境と設計モデルを組み合わせることにより，モデル検査ツールSPINで模倣関係の検査を行うことができる．
また，現在，提案手法を実現するツールの実装と，評価を行っている．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究では，OSEK/VDXと呼ばれる車載オペレーティングシステムを題材として用いている．そこで，平成24年度までにEvent-Bを用いてその形式仕様を作成した．また，これまでの研究により，題材である車載オペレーティングシステムの設計モデルは構築済みである．この設計モデルはPromelaにより記述されている．そこで，平成２５年度は，この形式仕様と設計モデルの対応関係の定義を行う予定であった．実際の平成２５年度の成果では，記述方式が異なる形式仕様と設計モデルの関係を，それぞれ，状態遷移システムに基づいて形式化して，それらの間の模倣関係により定義した．よって，平成２５年度に達成すべき当初の目標をクリアしていると言える．さらには，それらの間に模倣関係が存在することを，モデル検査ツールSPINで検査する手法も提案できた．これは，当初の予定では，平成26年度の前半で提案する予定であったが，約半年前倒しで達成することができた．これらのことから，(2)おおむね順調に進展している，と判断した．なお，平成26年度は，最終年度であるため，年度の前半でツールの実装を行い，後半で評価を行う予定である．
|
| Strategy for Future Research Activity |
平成２６年度は，最終年度であるため，年度の前半で手法の提案を完了し，後半で評価を行う．平成２５年度までに，モデル検査ツールSPINを用いて設計モデルが形式仕様に適合していることを検査する手法を提案した．Event-Bで作成された形式仕様は，潜在的に，無限の状態を持ち得る．一方で，Promelaによる記述は，有限状態に限られている．そこで，提案手法では，前者を有限状態に限定する境界(Bounds)を導入した．これにより，モデル検査ツールにより，設計モデルを形式仕様を用いて検査することが可能になった．この手法は，有界モデル検査(Bounded Model Checking)の一種とみなすことができる．有界モデル検査では，すべての状態を探索するのを諦めて，範囲を限定して網羅的に探索する．これにより，正しいという保証はできないが，誤りを見つける目的では，有効であると考えられている．また，本研究で提案した手法では，様々な境界を導入している．これにより，複数の境界を変化させることにより，探索の範囲を変化させることができ，柔軟に検査を行うことができると期待している．そこで，車載オペレーティングシステムを題材として，境界を変化させて実験を行う．そして，状態数などの効率，検出できる誤りの種類などの観点から提案手法の有効性を評価する．このような実験と評価を行うためには，ツールの実装が不可欠である．Event-Bによる形式仕様記述からPromelaにより記述された環境を手作業で作成するのは，とても時間がかかるからである．そこで，平成２６年度の前半は，車載オペレーティングシステムの題材が扱えるツールの実装を行う予定である．
|
