2012 Fiscal Year Research-status Report
形式手法の統合によるシームレスなソフトウェア開発手法の提案
| Project/Area Number |
24500035
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (20313702)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | 形式手法 / モデル検査 / 形式仕様 |
|---|
| Research Abstract |
本年度は，Event-Bで作成された形式仕様とPromelaで作成された設計モデルについて検討を行った．Promelaで作成された設計モデルは，モデル検査ツールSPINにより検査される．この際，時相論理や表明などにより，性質を記述する．しかしながら，実践的には，時相論理や表明による仕様の表現は限定的にならざるをえない．そこで，Promelaで作成された設計モデルが，Event-Bで作成された形式仕様を満たしているかどうか検証する手法について検討した．まず，設計モデルが形式仕様を満たしている，という事実を，それらの間の模倣関係で定義することにした．このような模倣関係が成立することを検証するためには，一般には，任意ステップの実行や任意の変数の値に関して証明を行わなければならず，帰納法や対話的な証明が必要になる．そこで，そのような証明を行う前に，限られた範囲で模倣関係が成立することをモデル検査ツールを用いて自動的に検査する手法を考案した．以下が，その概要である．
(1)Event-Bに出現する要素とPromelaに出現する要素を対応づける．
(2)Event-Bによる形式仕様から，その意味論(最弱事前条件)に基づいて，有限ステップの実行列を求める．
(3)その有限ステップの範囲でSPINにより設計モデルを検査する．この際，設計モデルを動作させるためのPromelaスクリプト，および，模倣関係であることを確認する表明を構成する．
また，OSEK/VDX OSの一部を対象とした実験も行った．現在，この手法の形式化を行っている．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
形式仕様記述とモデル検査を統合する具体的な一手法について検討をして，実験まで行えているため．これは，当初計画の平成25年度の課題であるが，前倒しで実現できている．一方で，実験は行えているが，十分に形式化が行えていないのが問題である．よって，おおむね順調に進展していると言える．
|
| Strategy for Future Research Activity |
Event-BとPromelaによる具体的な記述がすでに手中にあるのが，この研究の強みである．そこで，これらの具体的な記述に基づいて，実験を行いながら研究を進める予定である．
|
| Expenditure Plans for the Next FY Research Funding |
一部の物品が年度末まで納品されなかったことと，想定より金額が少なかった物品があった．納品されなかった物品については，次年度に購入予定である．
|
