基于ASP的CSP并发系统验证研究

传统并发通信顺序进程(CSP>性质的验证通常使用3个不同的模型层面，从而增加了系统的复杂性和验证 工具开发的难度;同时，主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质，这也降低了性质验 证的效率。首先将CSP程序转换为ASP程序，然后将CSP进程并发规则和以LTL/CTL公式表示的待验证性质转 换为ASP规则，从而建立了基于ASP验证CSP并发系统性质的统一框架。实验结果表明，基于ASP的CSP并发系 统验证技术易于实现，在保持较高验证效率的同时，能够支持在验证软件的一次执行中验证多条LTL/CTL公式。

ASP-based Verification of Concurrent Systems Described by CSP

Traditionally,the verification of properties of Communicating Sequential Processes (CSP) is carried out on three different levels of models, which increases the complexity and difficulty of developing verification tools. At the same time,mainstream tools for verifying concurrent systems cannot verify multiple properties at one run of the tools, which decreases the verification efficiency of the tools. To deal with the problems, this paper proposed an ASP-based u- nified framework for verifying concurrent systems described by CSP. The method first transforms CSPs into the An- saver Set Program, and then transforms the execution rules for concurrent CSP processes and the properties in the form of LTL/CTL formulae into the rules of ASP. At last, the properties can be verified by a computation of the answer sets of the resulting ASP program. It is shown that the ASP based method for verifying CSP concurrent system is easy to implement,is able to verify multiple LTL/CTL formulae at one execution of the verification software,and at the same time achieves acceptable time efficiency.