2010 Fiscal Year Annual Research Report
| Project/Area Number |
20500042
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
中島 震 国立情報学研究所, アーキテクチャ科学研究系, 教授 (60350211)
|
|---|
| Keywords | ソフトウェア工学 / ソフトウェア開発効率化・安定化 / 仕様記述・仕様検証 |
|---|
| Research Abstract |
本研究課題ではEvent-Bを用いて表現した要求モデルの自動検査方式に関する研究と、Event-Bを用いた要求のモデリング法に関する研究を中心に行った。前年度までの成果をもとに、Event-Bの最も一般的なイベント記述の方法であるany-where形式について述語抽象の方法を定式化した。さらに、Event-BのツールRODINを用いて上記の方法で必要となる抽象化計算を行う枠組みを考案した。抽象化した表現がProBでも解析可能であることを確認することで、抽象化のよる方法とProBが採用している有界化による方法の関係を考察した。モデリング法としては、イベント抽出、集合に基づく情報構造の整理、リファインメント手順の計画、の3つの点が難しく、一般のソフトウェア技術者が使用する阻害要因になっている。そこで、オブジェクト指向方法論をベースに、リファインメント計画シートと命名した新しい形式を提案し、これを用いたモデリング法を、産業界の技術者向けにまとめた。また、最近、オープンなシステムの要求モデル作成の難しさが指摘されていることから、利用者の振る舞いが関わるオープンなシステムを対象としてのモデリング事例を作成し、代数仕様の方法が自動解析に効果があることを示した。
本研究課題では、当初計画の通り、Event-Bに対する抽象化検証の方法を導入することが可能であることを示すことができた。また、研究の過程で、オープンなシステムの要求モデル作成へのEvent-B応用が未着手の領域であることがわかり、新たな研究課題として抽出することができた。
|
