左贵征,赵岭忠

基于ASP及稳定失败语义的CSP模型检测

左贵征,赵岭忠

(桂林电子科技大学计算机科学与工程学院,广西桂林 541004)

针对现有模型检测工具对活性描述不足、模型转换复杂,提出一种基于ASP及稳定失败语义的CSP模型检测方法。该方法采用时态逻辑LTL刻画性质,将进程的稳定失败模型和LTL公式转化为ASP,利用ASP求解器验证性质,实现一次运行验证多条性质。实验结果表明,该方法既扩大了基于稳定失败模型的活性验证范围,也避免了不同模型之间的转换。

通信顺序进程;线性时态逻辑;稳定失败语义;回答集程序设计

CSP[1]是由Hoare提出的一种代数语言,主要用于对并发系统进行刻画和验证。随着CSP在并发系统、通信协议等领域的广泛应用,CSP进程的形式化验证成为一个重要的研究课题。目前,CSP验证主要采用定理证明和模型检测,以操作语义和指称语义作为理论基础。

迹模型和稳定失败模型是2种典型的指称语义模型,迹模型描述了进程可执行的行为序列,可用于确定性进程的性质验证。然而,迹模型存在以下不足[2]:1)对所有进程统一采用行为序列描述,不能区分外部选择和内部选择,不能完全描述进程行为。如进程M1=(a→stop),M2=(b→stop),则进程M1| M2与进程的迹集均为{〈a〉,〈b〉}。2)不能验证不同环境下非确定性进程的相关性质。

基于此,Roscoe提出了CSP进程的稳定失败模型[2],该模型扩充了拒绝集描述进程拒绝执行的事件,实现了无发散进程的活性验证。文献[3]给出了一种用于CSP进程精化验证的交互式定理证明器CSP-mrover,在稳定失败模型中,可通过完备度量空间和完全偏序理论验证无边界非确定性的无限状态系统性质。……