论文部分内容阅读
CSP(Communicating Sequential Processes)是Hoare提出的一种代数语言，主要用于对并发系统进行描述与验证。主流的CSP模型检测工具包括FDR、PAT等。FDR通过操作语义将进程转化为相应的迁移系统，并依据迁移系统显式导出指称语义模型，转化过程较复杂且不易修改和扩展；性质描述采用CSP进程形式，与时态逻辑公式(LTL、CTL)相比，表达能力不强，特别是对活性的描述不足。PAT虽然采用LTL描述，但只能描述迹语义下系统性质，不能表示事件的可达性(available)。上述模型检测工具普遍不支持在验证工具的一次运行中验证多个性质。 为了解决以上问题，本文将ASP(Answer Set Programming)应用于基于稳定失败语义的CSP模型检测，将进程的稳定失败模型和LTL公式转化为ASP程序，将系统性质验证转化为回答集求解问题。采用LTL描述系统性质，扩大了稳定失败语义下系统性质验证范围。同时针对稳定失败模型只应用于无活锁的并发系统的特点，构造了基于ASP的CSP进程无活锁的静态分析算法，该算法保守地标记进程无活锁，可用于包含隐藏算子的并发系统的无活锁判定。具体地，主要研究内容如下： （1）基于ASP的并发系统无活锁的静态分析技术研究。基于稳定失败语义的模型检测只能验证无活锁的并发系统性质，为了验证进程的无活锁性，提出了基于ASP的CSP进程静态分析方法。通过对各种组合算子（选择，并发，隐藏和重命名）的分析，构造进程循环集合（进程的迹中可以无限次出现的事件组成的集合）和无活锁标记的ASP规则。循环集合还可用来确定隐藏哪些事件既不会导致进程发散，又减小了系统规模。 （2）基于ASP及稳定失败语义的并发系统CSP模型检测框架研究。确定并发系统无活锁后，为实现基于稳定失败语义的并发系统的性质验证，建立了基于ASP及稳定失败语义的CSP模型验证框架，将CSP模型检测转换为ASP回答集求解问题，实现了以并发方式一次运行验证多条性质。 （3）CSP进程的稳定失败模型到ASP程序的转换。给出CSP进程的ASP谓词表示，针对不同的组合算子（谨慎选择、外部选择、内部选择、并发和隐藏）构造了对应稳定失败模型的生成规则。 （4）稳定失败语义下基于ASP的LTL公式描述与验证。给出了稳定失败语义下LTL公式到ASP规则的转换，其中LTL公式增加了新的操作符available，使之能够描述稳定失败语义下系统性质。实验结果表明了本文提出的模型检测方法能够验证稳定失败语义下并发系统的安全性和活性，且实现一次运行验证多条性质。