2008 Fiscal Year Annual Research Report
| Project/Area Number |
20500042
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
中島 震 National Institute of Informatics, アーキテクチャ科学研究系, 教授 (60350211)
|
|---|
| Keywords | ソフトウェア工学 / ソフトウェア開発効率化・安定化 / 仕様記述・仕様検証 |
|---|
| Research Abstract |
本研究課題ではEvent-Bを用いて表現した要求モデルの自動検査に関する研究を実施した。Event-Bは20年以上の実績があるBメソッドを改良して開発上流工程のモデル記述を表現するために、並行性ならびに非決定性を明確に導入した。表現力が向上した反面、Bメソッドの検証法では、妥当性、安全性、進行性などの確認が難しくなった。本研究課題では抽象化支援モデル検査をEvent-Bに適用する方法を研究した。Event-Bに関する技術文書は欧州の研究プロジェクトRODINから公開されている。公開資料を調査し、掲載されている小規模例題を対象として、考案した方式の事例実験を代数仕様言語Maudeによって実施した。その結果、C言語やJavaによるプログラムのモデル検査で成功した述語抽象の方法をEvent-Bの体系の中で整理、実現できることがわかった。特に、ランキング抽象と呼ぶ方法を適用することで、安全性の確認だけではなく、妥当性の確認や進行性の確認も行うことができた。一方、ランキング抽象で必須となるランキング関数を発見することは難しいこと、より複雑なEvent-B記述(集合記法を用いた仕様)では述語抽象の方法だけではモデル検査の問題に帰着できないこと、などがわかった。上記の事例研究によって得た知見を欧州のBメソッドに関わる研究コミュニティが主催する国際ワークショップIM_FMTで発表した。Bメソッドの研究コミュニティは長い歴史を持つが初めての日本からの発表である。Event-Bは欧州の研究資金(FP7)で継続的に研究が続けられており、Bメソッドが実用的な成果を持つことから、その動向に注目が集まっている。本研究課題を国際交流のきっかけとすることを計画している。
|
