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

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

• 批准号: 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关于如何实现适当的抽象，提出的拟议的观察过渡（OTS：观察性过渡系统）被提出，适当地定义了数据类型和过程类型，以实现适当的架构，以实现适当的抽象。案例发展。 2。关于实现推理类型X探索-Type验证方法的方法，（1）如何在叛乱发现中组合（1）（IGF：指示指导性伪造）和（2）（2）基于推理的简介以及如何基于推理以及如何根据示例确认了基于探索的伪造。 （3）在电子商务方案的情况下，进行了研究，重点是确认基于示例的上述“推理类型×探索-Type验证方法”。具体而言，基于归纳方法，IKP（Internet密钥付款协议）被占用并确认了倒置发现（IGF）的有效性。在这种情况下，我们在Cafeobj语言系统中开发了形式的规格，研究了使用Maude语言系统的高效率搜索功能的方法，并为此开发了方法和支持工具。 4对于车载OS标准案例，AutoSar在Cafeobj的Osek/vdx规范中发布（Portal.osek-vdx.org/files/pdf/pdf/specs/os223.pdf）。在这种规范的开发中，确认了基于观察过渡系统（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