权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

面向对象分析模型定理证明系统的验证支持研究

基本信息

批准号：
12780204
负责人：
青木利晃
金额：
$ 1.28万
依托单位：
Japan Advanced Institute of Science and Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
2000
资助国家：
日本
起止时间：
2000 至 2001
项目状态：
已结题

项目摘要

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

F-Verifier is used to analyze the results of F-Verifier production in the previous year. The F-Verifier is made of the following materials: (1) The theorem proves that the HOL is automatically changed from one possible form to another; The proof of the problem on the HOL is implemented in the following way: This year, the library business support system analysis and preparation, F-Verifier application in the middle of the process related to the nature of the test The proof of the problem is the result of HOL. The solution of this problem is to investigate it. The reason for the proof of the word is high, and the reason for the analysis is high. For example, if a rule is valid, it is valid. The problem is solved by the advanced analysis method. The concept of creating a high-level model is organized according to the method of domain analysis. This year, the analysis of library business support systems has increased the level of abstraction and implementation. The result is that the axiom system is necessary. The expansion of the axiom system is related to future issues.