Methodology and Environment for Effectively Using Theorem Provers and Model Checkers
Methodology and Environment for Effectively Using Theorem Provers and Model Checkers
有效使用定理证明器和模型检查器的方法和环境
批准号：
18500019
负责人：
OGATA Kazuhiro
金额：
$2.78万
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2006
资助国家：
日本
项目状态：
已结题
起止时间：
2006 至 2008
中文摘要
翻译
点击翻译按钮获取中文摘要
英文摘要
証明支援系とモデル検査器を効果的に利用できるよう、定理証明向きのシステム仕様をモデル検査向きのシステム仕様に自動変換する方法を考案した。変換により、モデル検査向きのシステム仕様が大きくなりすぎて効果的にモデル検査ができなくなることを防ぐための工夫を行った。提案した変換方法の有効性を確認するため、電子商取引プロトコルiKPとMondex の検証実験に適用した。また、変換を支援する変換ツールの拡張性の高い実装方法も提案した。この実装方法では、複数の変換規則をモジュラーに組み入れることを可能にする。
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
登录
查看更多内容
Maude : 書換え論理に基づく計算機言語および処理系
Maude：基于重写逻辑的计算机语言和处理系统
Maude：基于重写逻辑的计算机语言和处理系统
DOI：
--
发表时间：
2008
期刊：
コンピュータソフトウェア(日本ソフトウェア科学会学会誌) 25-2
影响因子：
--
作者：
[緒方和博, 中村正樹, 二木厚吉]
通讯作者：
二木厚吉
Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm
通过案例研究模型检查分布式算法来比较 Maude 和 SAL
通过案例研究模型检查分布式算法来比较 Maude 和 SAL
DOI：
--
发表时间：
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 电子钱包系统形式分析的代数方法
Mondex 电子钱包系统形式分析的代数方法
DOI：
--
发表时间：
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：行为规范的自动不变证明者
Creme：行为规范的自动不变证明者
DOI：
--
发表时间：
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
DOI：
--
发表时间：
2006
期刊：
Proceedings of the 6th International Conference on Quality Software (6^<th> QSIC)
影响因子：
--
作者：
[Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, Kokichi Futatsugi]
通讯作者：
Kokichi Futatsugi
共 7 条
A divide and conquer approach to parallelization of LTL model checking
-
批准号：19H04082
-
项目类别：Grant-in-Aid for Scientific Research (B)
-
资助金额：$10.73万
-
财政年份：2019
-
负责人：OGATA Kazuhiro
-
依托单位：
Study of the mechanism of nucleosome-enhanceosome conversion
-
批准号：18K19305
-
项目类别：Grant-in-Aid for Challenging Research (Exploratory)
-
资助金额：$4.08万
-
财政年份：2018
-
负责人：OGATA Kazuhiro
-
依托单位：
Mechanism for regulation of DECODE complexes in gene activation
-
批准号：17054033
-
项目类别：Grant-in-Aid for Scientific Research on Priority Areas
-
资助金额：$67.58万
-
财政年份：2005
-
负责人：OGATA Kazuhiro
-
依托单位：
Molecular structural study for regulation on the activities of the hematopoietic transcriptional regulatory factors
-
批准号：14380296
-
项目类别：Grant-in-Aid for Scientific Research (B)
-
资助金额：$10.37万
-
财政年份：2002
-
负责人：OGATA Kazuhiro
-
依托单位：
海外基金