設計誤り検出のためのモデル検査を用いたソフトウェア解析システムの開発

使用模型检查进行设计错误检测的软件分析系统的开发

• 批准号: 14019055
• 负责人: 土屋 達弘
• 金额: $ 1.41万
• 依托单位: Osaka University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas
• 财政年份: 2002
• 资助国家: 日本
• 起止时间: 2002 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-14019055/
• 关键词: 記号モデル検査; 充足可能性判定; 設計誤り; 機能競合; 並行性

信頼性の高い情報システムを実現するためには,設計誤りを開発のできるだけ早期の段階で検出することが非常に重要となる.そのための手法として,システム上で起こりうる状態を網羅的に調べるモデル検査と呼ばれる方法が知られている.本課題では,近年になって開発されたモデル検査手法である限定モデル検査(Bounded Model Checking)を,非同期的な並行動作を有するソフトウェアシステムに適用するための研究を行った.限定モデル検査では,遷移関係を表現した論理関数からシステムの誤った振舞いを表現する一つの論理式を構成する.この論理式が充足可能であればシステムに設計誤りがあることを結論できる.しかし,従来の手法では,ソフトウェアシステムを対象とした場合,この論理式が非常に大きくなってしまい,効率良く検証が行えなかった.本研究では,平成13年度に開発した新しい論理式構成手法を改良し,1)これまで扱うことのできなかった種類の誤りの検出,及び,2)検証効率の向上,を実現した.1については,これまで安全性に関する誤りのみ検出可能であったものを,活性に関する性質についても可能にした.2については,論理式の生成前にシステムの動作規則の依存関係を予め考慮するような前処理を行うことで実現した.ペトリネットと通信電話サービスを具体的な検査対象として,これらの提案手法を実装した.実験の結果,従来の限定モデル検査や,他のモデル検査手法に比べ,非常に効率の良く設計誤りが検出できることが分かった.

The high level of information in the information system is very important. The method of searching and searching for information is known to all. This topic is aimed at the research of the application of the Bounded Model Checking (Bounded Model Checking), asynchronous parallel operation, and the development of the Bounded Model Checking (Bounded Model Checking). A logical expression for the expression of the transition relationship between a finite number and a finite number is presented. This logical expression is sufficient to be possible. The logic formula is very large, and the efficiency is good. This study is aimed at improving the construction of new logical expressions developed in Heisei 13. 1) Detection of errors in the types and types of logical expressions, and 2) Improvement of detection efficiency. 1) Detection of errors in the types and types of logical expressions related to safety, and 2) Detection of errors in the types and types of logical expressions related to activity. The dependency relationship between the operation rules of the system before the logical expression is generated is considered. The communication telephone service is requested to check the specific object and the proposal method. As a result, the results of this study are as follows: 1. The results of this study are as follows: 1. The results of this study are as follows: 1.

项目成果

土屋達弘, 菊野亨: "非同期並行システムに対するSATに基づくモデル検査"電子情報通信学会技術研究報告. 102・378. 31-36 (2002)

Tatsuhiro Tsuchiya，Toru Kikuno：“基于 SAT 的异步并行系统模型检查”IEICE 技术报告 102・378 (2002)。

濱田貴之, 土屋達弘, 中村匡秀, 菊野亨: "Detecting Feature Interactions in Telecommunication Systems by Symbolic Model Checking"Lecture Notes in Computer Science (Proc. of ICOIN 16). 2343. 641-651 (2002)

Takayuki Hamada、Tatsuhiro Tsuchiya、Masahide Nakamura、Toru Kikuno：“通过符号模型检查检测电信系统中的特征交互”计算机科学讲义（Proc. of ICOIN 16）。

田中崇浩, 土屋達弘, 菊野亨: "充足可能性判定を用いたモデル検査ツールの実装"電子情報通信学会技術報告. 102・27. 1-6 (2002)

Takahiro Tanaka、Tatsuhiro Tsuchiya、Toru Kikuno：“使用可满足性判断的模型检查工具的实现”IEICE 102・27（2002）。

土屋達弘, 中村匡秀, 菊野亨: "Symbolic Approaches to Feature Interaction Detection"Fastabstract : IEEE Conference on Dependable Systems and Networks. B46-B47 (2002)

Tatsuhiro Tsuchiya、Masahide Nakamura、Toru Kikuno：“特征交互检测的符号方法”Fastabstract：IEEE 可靠系统和网络会议 (2002)。

土屋達弘, 中村匡秀, 菊野亨: "Detecting Feature Interactions in Telecommunication Services with a SAT Solver"Proc. of 2002 Pacific Rim International Symposium on Dependable Computing (PRDC'02). 131-134 (2002)

Tatsuhiro Tsuchiya、Masahide Nakamura、Toru Kikuno：“使用 SAT 求解器检测电信服务中的特征交互”2002 年环太平洋国际可靠计算研讨会 (PRDC02) 的会议记录。