オブジェクト指向分析モデルの定理証明系を用いた検証支援に関する研究

2001 Fiscal Year Annual Research Report

• Project/Area Number: 12780204
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 青木 利晃 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (20313702)
• Keywords: オブジェクト指向分析 / 形式的手法 / 定理証明技術 / 検証 / 計算機支援環境

Research Abstract

平成13年度は、前年度作成した検証支援環境F-Verifierを用いて実験、及び実験結果の解析を行った。
F-Verifierでは、図形エディタで作成したオブジェクト指向分析モデルを、定理証明系HOLで取り扱い可能な形式に自動変換する。そして、HOL上で対話的証明を行うことにより、構築した分析モデルの検証を行う。本年度は、図書館業務支援システムの分析モデルを作成し、F-Verifierを用いていくらかの性質に関して検証を行った。その結果、HOL上での対話的証明にかかるコストが問題であることが判明した。そこで、この問題を解決する手法について考察した。
対話的証明のコストが高くなっていた理由は、分析モデルのHOLによる表現として用いているデータ型が原始的であるためであった。そのため、証明の際、粒度の細かい定理や推論規則を適用することになり、非常に多くの推論ステップを費やすことになった。この問題点を解決するためには、高級なデータ型をあらかじめ作成しておき、それを用いて分析モデルを作成することが有効である。このような高級なデータ型を作成する活動は、システム開発において対象領域に出現する概念を整理することに対応しており、領域分析手法と連携することにより効果的な手法となりうる。そこで、本年度は、図書館業務支援システムの分析モデルに出現するデータ型の抽象度を上げる実験も行った。その結果、前年度までに作成した公理系を拡張する必要があることが判明した。公理系の拡張に関しては今後の課題である。

Research Products

• [Publications] 青木利晃, 立石孝彰, 片山卓也: "定理証明技術のオブジェクト指向分析への適用"日本ソフトウェア科学会 コンピュータソフトウェア. Vol.18 No.4. 18-47 (2001)
• [Publications] Toshiaki Aoki, Takuya Katayama: "Prototype Execution of Independently Constructed Analysis Models"Automating the Object-Oriented Software Development. 25-33 (2001)
• [Publications] Toshiaki Aoki, Takaaki Tateishi, Takuya Katayama: "An Axiomatic Formalization of Object-Oriented Analysis Models"Practical UML-Based Rigorous Development Methods. 13-28 (2001)