Construction and verification of problem models in behavioral specifications

行为规范中问题模型的构建和验证

• 批准号: 15300007
• 负责人: FUTATSUGI Kokichi
• 金额: $ 9.73万
• 依托单位: Japan Advanced Institute Science and Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2003
• 资助国家: 日本
• 起止时间: 2003 至 2005
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15300007/
• 关键词: problem model; system verification; system safety; formal methods; behavioral specification; requirement specification; CafeOBJ

The following two important problems about construction and verification of problem models are investigated :(1) How to set an appropriate abstraction level in constructions of problem models and/or specifications.(2) How to combine interactive theorem proving technique and automatic searching based model checking technique in a collaborative way.Based on empirical studies on constructing and verifying problem models in several areas like railway signaling systems, component software systems, secure authentication systems, and etc., we got the following results.(1) Based on language constructs supported by CafeOBJ language, we have found that the distinction of abstract data types and abstract process types plays an important role in setting appropriate level in modeling/specification phase. Modeling/specification of process types are found to be complex and difficult than abstract data types, and we propose OTS (Observational Transition System) as a simple but powerful scheme for modeling/specifying process types. OTS is shown to be an effective and usable scheme for process types after applying it to several cases.(2) After studying several cases we have done, we found that (i) interactive theorem proving is more effective for proving some property hold, and (ii) automatic model checking is more effective for proving the some property does not hold (i.e. for finding counter examples). Based on this observation, we designed and developed an interactive tool which can support interactive proof (of proving some property hold) by finding counter examples with a model checking technique.

研究了以下两个有关问题模型构建和验证的重要问题：（1）如何在问题模型和/或规范的结构中设置适当的抽象水平。（2）如何将交互式定理证明技术和基于自动搜索的模型检查技术组合以协作方式以协作方式进行构建和验证诸如构造和验证的系统的构造系统等，以构造和验证型号的系统，并验证型号的系统，并验证型号的系统，并构造了构图，并构成了构图，并构成了构图，并构成了构图，构成了构图，构造了构图，构图以下结果。（1）基于Cafeobj语言支持的语言构造，我们发现抽象数据类型和抽象过程类型的区别在设置建模/规范阶段的适当水平方面起着重要作用。发现过程类型的建模/规范比抽象数据类型很复杂且困难，我们将OTS（观察转换系统）作为一种简单但功能强大的方案，用于建模/指定过程类型。 OTS被证明是将过程类型应用于几种情况后的有效且可用的方案。（2）研究了几种情况，我们发现（i）（i）交互式定理证明对证明某些属性持有更有效，并且（ii）自动模型检查更有效地证明某些属性无法持有（即寻找柜台示例）。基于此观察结果，我们设计并开发了一种交互式工具，可以通过使用模型检查技术找到反示例来支持交互式证明（证明某些属性保留）。

项目成果

Equational approach to formal analysis of TLS

• DOI: 10.1109/icdcs.2005.32
• 发表时间: 2005-01-01
• 期刊: 25th IEEE International Conference on Distributed Computing Systems, Proceedings
• 作者: Ogata, K;Futatsugi, K
• 通讯作者: Futatsugi, K

Equational Approach to Formal Verification of SET

SET 形式化验证的方程方法

• 发表时间: 2004
• 期刊: Proceedings of the 4th International Conference on Quality Software (4th QSIC),(IEEE Computer Society Press)
• 作者: Kazuhiro Ogata;Kokichi Futatsugi
• 通讯作者: Kokichi Futatsugi

項書き換えシステムにおける可簡約演算子とその応用

可约算子及其在术语重写系统中的应用

• 发表时间: 2005
• 期刊: 情報処理学会論文誌 : プログラミング 46 SIG 6(PRO25)
• 作者: 中村正樹;緒方和博;二木厚吉
• 通讯作者: 二木厚吉

Modeling and Verification of Hybrid Systems Based on Equations

基于方程的混合系统建模与验证

• 发表时间: 2004
• 期刊: Proc.of the IFIP 18th World Computer Congress TC10 Working Conference on Distributed and Parallel Embedded Systems
• 作者: Kazuhiro Ogara;Daigo Yamagishi;Takahiro Seino;Kokichi Futatsugi
• 通讯作者: Kokichi Futatsugi

Kazuhiro OGATA, Kokichi FUTATSUGI: "Formal analysis of the NetBill electronic commerce protocol"International Symposium on Software Security, LNCS. (To appera). (2004)

Kazuhiro OGATA、Kokichi FUTATSUGI：“NetBill 电子商务协议的形式分析”国际软件安全研讨会，LNCS。