Methodology and Environment for Effectively Using Theorem Provers and Model Checkers

有效使用定理证明器和模型检查器的方法和环境

• 批准号: 18500019
• 负责人: OGATA Kazuhiro
• 金额: $ 2.78万
• 依托单位: Japan Advanced Institute of Science and Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2006
• 资助国家: 日本
• 起止时间: 2006 至 2008
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18500019/
• 关键词: 仕様記述; 仕様検証; モデル検査; 仕様変換; 観測遷移システム; CafeOBJ、Maude; メタプログラミング; 定理証明; 変換; CafeOBJ; Maude; 変換器; 有界モデル検査; 数学的帰納法; 反例; 補題; IGF; 補題発見

証明支援系とモデル検査器を効果的に利用できるよう、定理証明向きのシステム仕様をモデル検査向きのシステム仕様に自動変換する方法を考案した。変換により、モデル検査向きのシステム仕様が大きくなりすぎて効果的にモデル検査ができなくなることを防ぐための工夫を行った。提案した変換方法の有効性を確認するため、電子商取引プロトコルiKPとMondex の検証実験に適用した。また、変換を支援する変換ツールの拡張性の高い実装方法も提案した。この実装方法では、複数の変換規則をモジュラーに組み入れることを可能にする。

In this paper, we use the theory and theorem to make clear that the support system is used to make sure that the method of automatic training is used in the research of the method of automatic training. In the first place, please tell me that you are going to pay attention to the situation in the first place. The proposed method has the advantages of confirming the usage of the information, and the electronic merchant will introduce the information of the iKP to the Mondex of the customer. Please support the proposal for the installation of high-quality equipment. It is not possible to install the method, copy the rules, and change the number of rules.

项目成果

Maude : 書換え論理に基づく計算機言語および処理系

Maude：基于重写逻辑的计算机语言和处理系统

• 发表时间: 2008
• 期刊: コンピュータソフトウェア(日本ソフトウェア科学会学会誌) 25-2
• 作者: 緒方和博;中村正樹;二木厚吉
• 通讯作者: 二木厚吉

Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm

通过案例研究模型检查分布式算法来比较 Maude 和 SAL

• 发表时间: 2007
• 期刊: IEICE TRANSACTIONS on Fundamental of Electronics, Communications and Computer Science E90-A(8)
• 作者: Takeshi Tokuyama (編集;単独);須鎗弘樹;Kazuhiro Ogata and Kokichi Futatsugi
• 通讯作者: Kazuhiro Ogata and Kokichi Futatsugi

Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System

Mondex 电子钱包系统形式分析的代数方法

• 发表时间: 2007
• 期刊: Proc.of the 6th Int'l Conf on Integrated Formal Methods LNCS4951
• 作者: W.Kong;K.Ogata;K.Futatsugi
• 通讯作者: K.Futatsugi

Creme: An Automatic Invariant Prover of Behavioral Specifications

Creme：行为规范的自动不变证明者

• 发表时间: 2007
• 期刊: International Journal of Software Engineering And Knowledge Engineering 17(6)
• 作者: Masahiro Nakano;Kazuhiro Ogata;Masaki Nakamura and Kokichi Futatsugi
• 通讯作者: Masaki Nakamura and Kokichi Futatsugi

Automating Invariant Verification of Behavioral Specifications

自动验证行为规范的不变性

• 发表时间: 2006
• 期刊: Proceedings of the 6th International Conference on Quality Software (6^<th> QSIC)
• 作者: Masahiro Nakano;Kazuhiro Ogata;Masaki Nakamura;Kokichi Futatsugi
• 通讯作者: Kokichi Futatsugi