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

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

• 批准号: 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)に基づく形式仕様開発方法論の有効性を確認した。

The following results were achieved during the ongoing research and development of innovative personal-verification technology that proves that it is possible to verify problem persons (organizations, rules, activities, and processing persons and entities in the problem domain and application domain) in the SCORE method. 1. The abstract degree realization method is used to determine whether the abstract degree realization method is suitable for the definition of the abstract type and the abstract type. 2. Inference type × exploration type method and realization method;(1) Inference method and basic guidance method;(2) Inference method and basic guidance method;(3) Inference method and basic guidance method;(4) Inference method and basic guidance method;(5) Inference method and basic guidance method. 3. Electronic Quotient Quotation Case Study, Inference Type × Exploratory Type Verification Method, Example, Basis, Confirmation, Focus, and Research Specific iKP(Internet Keyed Payment Protocols) are available on the Internet, in the Internet and in the Internet. This case development is based on the development of CafeOBJ speech system, the development of Maude speech system and the exploration of its high efficiency function. 4. The standard case of in-vehicle OS, AUTOSAR, is open to the world, and the recognition of OSEK/VDX specification (portal.osek-vdx.org/files/pdf/specs/os223.pdf) is high. The description of CafeOBJ language is open to the public. The effectiveness of the methodology for the development of this model is confirmed by the measurement and migration system (OTS).

项目成果

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

A Note on On the Construction of Boolean Functions with Optimal Algebraic Immunity

注释

• 期刊: IEICE Transactions on Fundamentals of Electronics Communications and Computer Sciences
• 影响因子: 0.5
• 作者: Yuan Li1;Haibin Kan1;Futatsug, K.2
• 通讯作者: Futatsug, K.2

Conformance Verification between Web Service Choreography and Imple mentation Using Learning and Model Checking

使用学习和模型检查来验证 Web 服务编排和实现之间的一致性

• 发表时间: 2011
• 作者: Warawoot Pacharoen;Toshiaki Aoki;Athasit Surarerks;Pattarasinee Bhattarakosol
• 通讯作者: Pattarasinee Bhattarakosol

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