| 研究概要 |
平成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では公理系を自動生成するため,非常に効率よく検証の前準備を行うことができた.しかしながら,証明には非常に多くのステップを費した.来年度は証明ステップを減少させるための手法について考察を行う予定である.
|
