|
本研究課題では、Event-Bを用いて表現した要求モデルの自動検査に関する研究を実施した。初年度に得た知見をもとに、自動検査対象となるイベント記述の範囲を広げた。特に、when形式に加えて、any-where形式を取り扱う方式を考察した。方式のポイントは本質的に無限のデータ空間を表現するany-where形式を有限スコープに制限することである。これは一般に有界モデル検査や述語論理を対象とする有界探索による解析と同様な考え方にたつ。与えられたany-where形式の記述から、等価変換を行って、有界化しやすい形式に変換し、その後、有界化ならびに述語抽象の方法を組み合わせる。簡単な例題を対象として方式を確認した。また、Event-Bを用いた要求モデル作成の知見を得ること、ならびに自動検査の研究を進めるための具体的な事例を作成すること、という目的から、中規模事例を作成した。組込みソフトウェアの要求モデルで重要な多重割り込みシステムの例題を取り扱った。これは、複数の形式手法を比較検討するベンチマーク問題として考案したものである。本中規模事例の作成過程で、リファインメントがモデリングに与える影響についても知見を得ることができた。なお、産業界でもEvent-Bへの関心が高まってきている。本研究で得られた知見がアウトリーチ活動に役立つ。自動検査に関わる学術研究と並行してEvent-B適用ノウハウの蓄積が重要になってきている。
|
