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

2000 Fiscal Year Annual Research Report

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

Research Abstract

平成12年度の研究成果は以下の3つである.
1.F-Modelの形式から定理証明系HOLにおいて取扱可能な公理系への変換法を定義した.
公理系には局所不変性公理,大域不変性公理,イベント導入公理,イベント通信公理と呼ばれる4つの公理を導入した.これらの公理は,F-Modelで記述したオブジェクトが属性を更新しながら互いに協調動作する世界で,属性値に関する不変性制約の正当性を証明するためのものである.また,構築したF-Modelで属性と関数に対してHOLにおける表現を割り当てることにより,公理系を自動生成できることを示した.
2.HOLを用いたGUIベースの検証支援環境F-Verifierを開発した.
F-Verifierでは,Javaで実装したGUIを用いてF-Modelを構築する.F-Modelは集合と関数の体系を用いて形式的に定義されているが,GUIをインターフェースとすることにより,直観的な図的表現で分析を行うことができる.GUIで構築したF-Modelは一旦リポジトリに格納される.そして,F-Verifierの公理系自動生成器により,1.で提案した変換法に基づいて,HOLの公理系を自動生成する.
3.F-Verifierを用いて,図書館システムの分析モデルを構築し,検証を行った.
2.で開発したF-Verifierを用いて,図書館における本管理を支援するシステムを対象にした実験を行った.F-Verifierでは公理系を自動生成するため,非常に効率よく検証の前準備を行うことができた.しかしながら,証明には非常に多くのステップを費した.来年度は証明ステップを減少させるための手法について考察を行う予定である.

Research Products

• [Publications] 立石孝彰,青木利晃,片山卓也: "オブジェクト指向分析モデルの検証と公理系の提案"情報処理学会ソフトウェア工学研究会 研究報告 2000-SE-127. 39-45 (2000)
• [Publications] 立石孝彰,青木利晃,片山卓也: "HOLを用いたオブジェクト指向分析モデルの検証"ソフトウェア工学の基礎IV(FOSE2000). 117-124 (2000)
• [Publications] T.Tateishi,T.Aoki and T.Katayama: "An Axiomatic System For Verifying The Object-Oriented Analysis Model"SCI2000 Proceedings VolumeIII. 662-667 (2000)