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

项目名称： 基于ASP的并发系统CSP模型验证研究

项目编号： No.61262008

项目类型： 地区科学基金项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 赵岭忠

作者单位： 桂林电子科技大学

项目金额： 46万元

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

中文关键词： 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, reali

英文关键词： CSP；model checking；denotational semantics；logic programming；debugging