论文部分内容阅读
并发系统是现实世界中一类重要的复杂系统，已广泛应用于军事、交通、商业和服务业中，纵观现代软件行业，从操作系统到互联网，并发程序无处不在。虽然并发程序在当前有着广泛的应用，但程序的并发特性也使得程序语义具有不确定性，从而使并发程序性质的验证研究较顺序程序要困难得多。模型检测是主流的并发系统验证技术。但多数并发系统模型验证工具不支持在系统的一次运行中验证多个性质，从而也降低了性质验证的效率。该问题在现有的主流模型检测框架内很难克服。 通信顺序进程(Communication sequential process,CSP)是一种具有严格数学理论支持的描述并发进程之间相互作用模式的进程代数语言，已经在网络协议建模、并发系统验证以及计算机软硬件设计方面得到广泛的应用。本文研究以 CSP语言描述的并发系统性质的验证问题，构建基于回答集编程(Answer Set Programming，ASP)的CSP并发系统验证框架，解决上述讨论的并发系统验证方法中的问题。具体地，本文主要研究成果如下： (1)提出了将CSP模型转换为ASP程序的方法，讨论了CSP进程的顺序、循环和选择结构的ASP程序描述，给出了CSP的并发执行规则的ASP描述。研究了把待验证系统性质转化为ASP规则的技术，给出了LTL、CTL公式到ASP规则的转换方法。 (2)在此基础上开发了基于ASP的CSP并发系统验证原型系统。实验结果表明该技术易于实现，在保持较高验证效率的同时，能够支持在验证软件的一次执行中验证多条LTL/CTL公式。 (3)提出了CSP并发系统性质不满足时生成反例的技术，把ASP程序支撑原因分析技术应用于 CSP模型验证性质反例生成研究，给出了相应的反例生成算法，实例表明了该技术的有效性。