基于进程迹的CSP模型验证框架  

Framework for Model Checking CSP with Traces of Processes

作　　者：赵岭忠[1] 翟仲毅[1] 钱俊彦[1] 

机构地区：[1]桂林电子科技大学计算机科学与工程学院,桂林541004

出　　处：《计算机科学》2013年第11期181-186,221,共7页Computer Science

基　　金：国家自然科学基金(61262008;61063002);广西自然基金(2011GXNSFA018166;2011GXNSFA018164);广西可信软件重点实验室基金(kx201113)资助

摘　　要：CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂;性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框架,其性质采用通用的规范方法LTL进行描述。利用ASP(Answer Set Programming)技术实现了一个CSP验证系统。实验表明,与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,在性质不满足时还可提供反例。Communicating Sequential Processes is a classic method for describing concurrent systems and network secu- rity protocols. The verification for CSP is a complex conversion process, which translates processes into a label transi- tion system and describes the properties to be verified with traces. The main problem of the method is in the description of liveness properties. This paper proposed a framework for model checking CSP with traces, in which properties are specified by LTL, a universal property specification language. Finally, a verification system for CSP was implemented with answer set programming. It is shown that the ability of the system for describing CSP processes is more powerful and the verification accuracy of the system is higher than the similar system developed previously. When a property is not qualified, the system returns counterexamples for the property.

关 键 词：通信顺序进程(CSP) 并发系统 迹模型 回答集编程(ASP) 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]