A study on a reliable automatic verification tool for concurrent systems

一种可靠的并发系统自动验证工具的研究

• 批准号: 20500023
• 负责人: ISOBE Yoshinao
• 金额: $ 2.25万
• 依托单位: National Institute of Advanced Industrial Science and Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2008
• 资助国家: 日本
• 起止时间: 2008 至 2010
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20500023/
• 关键词: 並行システム; プロセス代数; 自動解析ツール; 記号処理; 状態数削減; 無限状態システム; 定理証明器; モデル検査器; 値渡しプロセス代数; 解析; モデル検査; 検証

This work aims at developing tools which analyze concurrent systems automatically like model-checkers and symbolically like theorem-provers, in order to support designs of the systems. Then, we have studied on such analysis-tools from two points of views : (1) automatizing proofs in theorem-provers and (2) introducing symbolic computation to model-checkers. In the former (1), we showed that proofs in CSP-Prover, which is a theorem-prover for a concurrency theory called CSP, can be automatized by implementing a model-checking algorithm to CSP-Prover. In the latter (2), we presented a method for automatically analyzing the whole behaviors from structures of concurrent systems and behaviors of component-processes by symbolic computation, and we implemented the analysis-method in a prototype-tool called CONPASU. For example, CONPASU can automatically generate symbolic-labeled transition graphs, which are useful for understanding the behaviors, from concurrent systems with infinite-states.

这项工作的目的是开发自动分析并发系统的工具，例如模型检查器和象征性的定理证明器，以支持系统的设计。然后，我们从两个角度研究了此类分析工具：（1）在定理证明器中自动化证明；（2）向模型检查器引入符号计算。在前 (1) 中，我们展示了 CSP-Prover 中的证明（CSP-Prover 是称为 CSP 的并发理论的定理证明器），可以通过在 CSP-Prover 中实现模型检查算法来实现自动化。在后者（2）中，我们提出了一种通过符号计算自动分析并发系统结构和组件进程行为的整体行为的方法，并在称为 CONPASU 的原型工具中实现了该分析方法。例如，CONPASU 可以自动生成符号标记的转换图，这对于理解具有无限状态的并发系统的行为很有用。

项目成果

The Stable Revivals Model in CSP-Prover

• DOI: 10.1016/j.entcs.2009.08.021
• 发表时间: 2009-09
• 作者: D. Gift Samuel;M. Roggenbach;Yoshinao Isobe

Verifying Train Control Software--An exercise in SAT-based Model Checking

验证列车控制软件--基于SAT的模型检查练习

• 发表时间: 2009
• 作者: 沖忠親;田岡智志;渡邉敏正;磯部祥尚
• 通讯作者: 磯部祥尚

A Prototype Tool for Analyzing Concurrent Processes -- Towards Automatic Generation of Specifications

分析并发流程的原型工具——迈向规格说明的自动生成

• 发表时间: 2010
• 作者: Kamiyama;Naoyuki;磯部祥尚
• 通讯作者: 磯部祥尚

CONPASU-tool : A Concurrent Process Analysis Support Tool based on Symbolic Computation

CONPASU-tool ：基于符号计算的并发过程分析支持工具

• 发表时间: 2011
• 期刊: Communicating Process Architectures 2011 (IOS Press)
• 作者: 宗崎良太;田尻達郎;田中桜;木下義晶;古賀友紀;住江愛子;松崎彰信;原寿郎;田口智章;Zhi-Zhong Chen;山田貴志;磯部祥尚
• 通讯作者: 磯部祥尚

CONPASUのホームページ

康帕苏主页