基于ASP的CSP模型验证性质反例生成技术研究

【引言】通信顺序进程( CSP) 是一种具有严格数学理论支撑的描述并发进程之间相互作用模式的进程代数语言，已经在网络协议建模、并发系统验证、特别是计算机安全和硬件设计方面得到了广泛应用。CSP 并发进程的验证通常采用模型检测技术。牛津大学计算机计算实验室开发了CSP 进程模型检测工具FDR。FDR 验证系统是否满足某性质的基本思想是: 利用状态机判断是否存在一个符合该性质的精化迁移系统。Garavel等人注意到CSP 进程模型检测中高级语言模型和低层实现模型设计目标的差异性，以及由此造成的直接把高级语言模型转换为低层模型的困难性和复杂性，提出在高级语言与实现模型之间增加必要过渡的中介模型。目前，并发系统模型检测技术还存在以下问题，即主流的并发系统模型检测算法( 如基于Kripke 结构和Petri 网的模型检测) 不支持在验证工具的一次运行中验证多个性质，该特点直接限制了系统性质验证效率的提高: a) 多次运行验证工具会造成大量的上下文切换的开销; b) 由于即使待验证的性质式存在相同的子公式，也必须分开多次处理，从而造成多次处理同一子公式产生的重复计算开销。以上问题在现有的主流模型检测框架( 如基于自动机的模型检测、基于图搜索和不动点计算的模型检测) 内很难克服。