研究課題
基盤研究(C)
本年度は，Event-Bで作成された形式仕様とPromelaで作成された設計モデルについて検討を行った．Promelaで作成された設計モデルは，モデル検査ツールSPINにより検査される．この際，時相論理や表明などにより，性質を記述する．しかしながら，実践的には，時相論理や表明による仕様の表現は限定的にならざるをえない．そこで，Promelaで作成された設計モデルが，Event-Bで作成された形式仕様を満たしているかどうか検証する手法について検討した．まず，設計モデルが形式仕様を満たしている，という事実を，それらの間の模倣関係で定義することにした．このような模倣関係が成立することを検証するためには，一般には，任意ステップの実行や任意の変数の値に関して証明を行わなければならず，帰納法や対話的な証明が必要になる．そこで，そのような証明を行う前に，限られた範囲で模倣関係が成立することをモデル検査ツールを用いて自動的に検査する手法を考案した．以下が，その概要である．(1)Event-Bに出現する要素とPromelaに出現する要素を対応づける．(2)Event-Bによる形式仕様から，その意味論(最弱事前条件)に基づいて，有限ステップの実行列を求める．(3)その有限ステップの範囲でSPINにより設計モデルを検査する．この際，設計モデルを動作させるためのPromelaスクリプト，および，模倣関係であることを確認する表明を構成する．また，OSEK/VDX OSの一部を対象とした実験も行った．現在，この手法の形式化を行っている．
2: おおむね順調に進展している
形式仕様記述とモデル検査を統合する具体的な一手法について検討をして，実験まで行えているため．これは，当初計画の平成25年度の課題であるが，前倒しで実現できている．一方で，実験は行えているが，十分に形式化が行えていないのが問題である．よって，おおむね順調に進展していると言える．
Event-BとPromelaによる具体的な記述がすでに手中にあるのが，この研究の強みである．そこで，これらの具体的な記述に基づいて，実験を行いながら研究を進める予定である．
一部の物品が年度末まで納品されなかったことと，想定より金額が少なかった物品があった．納品されなかった物品については，次年度に購入予定である．
すべて 2013 2012
すべて 雑誌論文 (3件) (うち査読あり 3件) 学会発表 (7件) 図書 (1件)
IEICE Transactions
巻: Vol.E95-D,No.7 ページ: pp.1882-1893
10.1587/transinf.E95.D.1882.
日本ソフトウェア科学会 学会誌 コンピュータソフトウェア
巻: Vo.29, No.3, ページ: pp.121-142
巻: Vol.95-A, No.9 ページ: pp.1451-1460
10.1587/transfun.E95.A.1451.
