Research on Design Verification Process Using Model Checking

使用模型检查的设计验证过程研究

• 批准号: 19500035
• 负责人: TAHARA Yasuyuki
• 金额: $ 2.66万
• 依托单位: The University of Electro-Communications (2008)National Institute of Informatics (2007)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2007
• 资助国家: 日本
• 起止时间: 2007 至 2008
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19500035/
• 关键词: 計算機システム; 情報システム; ソフトウェア開発効率化・安定化; ソフトウェア学; ソフトウェア検証

近年、ソフトウェアは大規模化、複雑化が進んでいることから、高信頼でかつ安全なソフトウェア設計を実施するために、モデル検査技術が有望視されている。本研究では、開発者に分かりやすい設計と、モデル検査に必要な抽象的数学理論のギャップを縮めるために、既存技術であるTemplate Semantics をベースとした、形式モデルの意味論を参照・変更可能な設計モデル検証プロセスを考案し、そのプロセスに基づく開発支援ツールのプロトタイプを開発した。

In recent years, the large-scale and complex development of software and hardware has become more and more important, and the implementation of security and hardware design has become more and more important. This study is divided into three parts: design, development, research, abstract mathematical theory, existing technology, Template Semantics, formal semantics, reference, more likely design, research, research, development and support.

项目成果

開発プロセスにおけるセキュリティ関心事の分離に向けて

致力于分离开发过程中的安全问题

• 发表时间: 2008
• 作者: 田原 康之;吉岡 信和;田口 研治;本位田 真一
• 通讯作者: 本位田 真一

ソフトウェア科学基礎

软件科学基础

• 发表时间: 2008
• 作者: 磯部祥尚;粂野文洋;櫻庭健年;田口研治;田原康之(著);田中譲(監修);本位田真一(シリーズ監修)
• 通讯作者: 本位田真一(シリーズ監修)

SPINによる設計モデル検証

使用 SPIN 验证设计模型

• 发表时间: 2008
• 作者: Kouji Kozaki;Takeru Hirota;Riichiro Mizoguchi;吉岡信和,青木利晃,田原康之
• 通讯作者: 吉岡信和,青木利晃,田原康之

Education Course of Practical Model Checking

实用模型检验教育课程

• 发表时间: 2008
• 作者: Yasuyuki Tahara;Nobukazu Yoshioka;Kenji Taguchi;Toshiaki Aoki;Shinichi Honiden
• 通讯作者: Shinichi Honiden