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