証明スコア法に基づく革新的仕様検証技術の研究

基于证明评分法的创新规范验证技术研究

• 批准号: 23240004
• 负责人: 二木 厚吉
• 金额: $ 9.65万
• 依托单位: Japan Advanced Institute of Science and Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (A)
• 财政年份: 2011
• 资助国家: 日本
• 起止时间: 2011 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-23240004/
• 关键词: 仕様記述・仕様検証; 形式手法; 形式仕様; 問題仕様; ソフトウェア工学; 証明スコア; CafeOBJ; 観測遷移システム

証明スコア法により問題仕様(問題領域や応用領域における組織、規則、活動、処理の仕様やモデル)の検証を可能とする革新的仕様検証技術の開発を目指して研究を行い、以下の成果を得た。1適切な抽象度の実現法について、提案している観測遷移シヌテム(OTS:Observational Transition System)がデータ型とプロセス型を適切に定義することで、適切な抽象度を実現する一般的なスキーマと成り得ることを、実用規模の事例開発を通じて確認した。2推論型×探索型検証法の実現法について、(1)帰納法に基づく反例発見法(IGF:Induction Guided Falsification)と(2)推論に基づく抽象化と探索に基づく反例発見を組み合わせる方法、の2つの方法が有効であることを例題に基づき確認した。3電子商取引プロトコル事例については、上記の「推論型×探索型検証法」を実例に基づき確認することに焦点を当てて研究を行った。具体的にはiKP(Internet Keyed Payment Protocols)を取り上げ、帰納法に基づく反例発見法(IGF)の有効性を確認した。この事例開発では、CafeOBJ言語システムで形式仕様を開発し、Maude言語システムの高効率の探索機能を利用する方法論についても研究を行い、そのための方法論と支援ツールも開発した。4車載OS標準事例については、AUTOSARが公開し世界的に認知度が高いOSEK/VDX仕様(portal.osek-vdx.org/files/pdf/specs/os223.pdf)に対して、CafeOBJ言語で記述された形式仕様を開発した。この仕様開発において、観測遷移システム(OTS)に基づく形式仕様開発方法論の有効性を確認した。

我们进行了研究，目的是开发创新的规范验证技术，以使用证明分数方法来验证问题规格（在问题领域和应用领域的组织，规则，活动和处理的规格和模型），并实现以下结果。 1。我们通过实际案例开发确认，提议的观察过渡系统（OT）可以是一种通用模式，可以通过正确定义数据类型和过程类型来实现适当的抽象。我们基于示例问题确认了两推 - 类型X搜索类型验证方法的有效性，该方法有效：（1）基于诱导的诱导指导性伪造（IGF），以及（2）一种结合基于推理的抽象和基于搜索的基于搜索的comply-example发现的方法。 3以电子商务协议的示例，我们进行了研究，重点是基于实际示例确认上述“推理类型X搜索类型验证方法”。具体来说，我们采用了IKP（Internet键付款协议），并根据归纳确认了反例检测方法（IGF）的有效性。在这种情况下，我们在Cafeobj语言系统上开发了正式的规范，还研究了一种利用Maude语言系统高效搜索功能的方法，并为此开发了一种方法和支持工具。 4A对于标准车辆内部的操作系统，AutoSar已开发了用Cafeobj语言编写的格式规范，用于OSEK/VDX规范（Portal.osek-vdx.org/files/pdf/pdf/specs/os223.pdf），由AutoSar在全球范围内公开识别。在这种规范的开发中，确认了基于观察过渡系统（OT）的形式规范开发方法的有效性。

项目成果

Automated Adaptor Generation for Services Based on Pushdown Model Checking

• DOI: 10.1109/ecbs.2011.33
• 发表时间: 2011-04
• 期刊: 2011 18th IEEE International Conference and Workshops on Engineering of Computer-Based Systems
• 作者: Hsin-hung Lin;Toshiaki Aoki;T. Katayama

Formalization of Risks and Control Activities in Business Process

业务流程中风险和控制活动的形式化

• 发表时间: 2011
• 期刊: Proc.of 2011 World Congress on Computer Science and Information Engineering (CSIE 2011), Lecture Notes in Electrical Engineering, Springer
• 作者: Yasuhito Arimoto;Shusaku Iida;Kokichi Futatsugi
• 通讯作者: Kokichi Futatsugi

A Modeling Framework to Support Internal Control

支持内部控制的建模框架

• 发表时间: 2011
• 期刊: Proc.of The Fifth International Conference on Secure Software Integration and Reliability Improvement Companion (IEEE SSIRI-C 2011)
• 作者: Takafumi Komoto;Kenji Taguchi;Haralambos Mouratidis;Nobukazu Yoshioka;Kokichi Futatsugi
• 通讯作者: Kokichi Futatsugi

Translation of State Machines from Equational Theories into Rewrite Theories with Tool Support

在工具支持下将状态机从方程理论转化为重写理论

• DOI: 10.1587/transinf.e94.d.976
• 发表时间: 2011
• 期刊: IEICE Transactions on Information and Systems
• 影响因子: 0.7
• 作者: Min Zhang;Kazuhiro Ogata;Masaki Nakamura
• 通讯作者: Masaki Nakamura

Conformance Testing for OSEK/VDX Operating System Using Model Checking

• DOI: 10.1109/apsec.2011.26
• 发表时间: 2011-12
• 期刊: 2011 18th Asia-Pacific Software Engineering Conference
• 作者: Jiang Chen;Toshiaki Aoki