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

In order to improve the efficiency of verifying the CSP models for concurrent systems, an ASP based verification framework will be established, intended to achieve the following objectives: 1) verifying multiple properties described by temporal logic in only one run of the verification tool to be developed; 2) dynamically estimating the effects of the changes in the original CSP model on the properties that were verified; and 3) supporting verification of properties of a system in an incremental style. Based on the sharing analysis of the LTL/CTL formulas, remove the computation cost caused by multiple processing of the same sub-formula. Based on the semantics of CSP, LTL/CTL formulas, and ASP programs, construct transformation rules from CSP processes and temporial logic formulas to ASP rules. Based on the semantics theory of ASP programs, prove the correctness of the verifying method. Based on the justification generation techniques for ASP programs, generate counter-examples when a property does not hold for the system under consideration, and analyze the effects of the changes in the system model on the properties that held before. Based on the semantic relationship between CSP processes and ASP programs, develop technologies that aid the debugging of the CSP processes. Based on the ASP knowledge base, realize the incremental verification of system properties. The method for verifying CSP models for concurrent systems that is to be developed in this project will achieve all the above features, providing a prospective, novel and efficient method for the verification of concurrent systems. Finally, the tool to be developed will be potentially very useful in the area of development of software for concurrent systems.

为了提高并发系统CSP模型验证的效率，支持在验证工具的一次运行中验证多个性质、动态评估系统模型改变对已验证性质的影响、并增量式地验证系统性质，建立基于ASP的并发系统CSP模型验证框架。基于时态逻辑LTL/CTL公式的可共享性分析，消除同一子公式重复处理的计算开销；基于CSP、LTL/CTL公式和ASP程序语义，建立CSP进程及时态逻辑公式到ASP规则的转换；基于ASP程序语义理论，证明验证方法的正确性；基于ASP支撑原因分析技术，在待验证性质不满足时产生反例，以及在系统模型改变时，分析对已验证性质的影响；基于CSP进程和ASP程序间的语义联系，开发并发系统CSP模型的调试辅助技术；并基于ASP知识库技术实现系统性质的增量式验证。项目将研究的基于ASP的并发系统CSP模型验证技术将同时具有以上特征，具有学术创新性、前瞻性和实际应用前景。

针对现有CSP模型检测工具不能在验证工具的一次运行中验证多个性质、也不能动态评估系统模型改变对已验证性质的影响、更不能增量式地验证系统性质的特点，在分析现有CSP模型检测技术的基础上，提出并建立了基于ASP 的并发系统 CSP 模型验证框架。基于对CSP语义的分析，我们提出了适合适用于CSP进程模型验证的基于关键迹的CSP进程语义；基于 CSP、LTL/CTL 公式和 ASP 程序语义，本项目建立了 CSP 进程及时态逻辑公式到 ASP 规则的转换；基于 ASP 程序语义理论，证明了验证方法的正确性；基于 ASP支撑原因分析技术，在待验证性质不满足时产生反例，以及在系统模型改变时，分析对已验证性质的影响；基于 CSP 进程和 ASP 程序间的语义联系，开发并发系统 CSP 模型的调试辅助技术；并基于 ASP 知识库技术实现系统性质的增量式验证。项目提出的基于 ASP 的并发系统 CSP 模型验证技术基本具备了以上特征，为未来开发新的CSP模型检测工具提供了一些基础。此外，在本课题的支持下对硬件的可靠性验证、web服务软件的构造等问题也进行了一些探讨，获得了一些初步成果。