摘要
传统并发通信顺序进程(CSP)性质的验证通常使用3个不同的模型层面,从而增加了系统的复杂性和验证工具开发的难度;同时,主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质,这也降低了性质验证的效率。首先将CSP程序转换为ASP程序,然后将CSP进程并发规则和以LTL/CTL公式表示的待验证性质转换为ASP规则,从而建立了基于ASP验证CSP并发系统性质的统一框架。实验结果表明,基于ASP的CSP并发系统验证技术易于实现,在保持较高验证效率的同时,能够支持在验证软件的一次执行中验证多条LTL/CTL公式。
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 unified framework for verifying concurrent systems described by CSP.The method first transforms CSPs into the Answer 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.
出处
《计算机科学》
CSCD
北大核心
2012年第12期125-132,共8页
Computer Science
基金
国家自然科学基金(61063002)
广西自然基金(2011GXNSFA018166
2011GXNSFA018164)
武汉大学软件工程国家重点实验室开放基金(SKLSE2010-08-06)
广西可信软件重点实验室基金项目(kx201113)
广西研究生教育创新计划项目(2010105950812M28)资助
关键词
通信顺序进程
回答集编程
LTL
CTL
Communicating sequential processes
Answer set program
LTL/CTL
