基于进程迹的csp模型验证框架

csp(communicatingsequentialprocesses)是构建并发系统和网络安全协议的经典方法。当前主流的csp模型验证方法需将进程转化为迁移系统,转化过程比较复杂；性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的csp模型验证框架,其性质采用通用的规范方法ltl进行描述。利用asp(answersetprogramming)技术实现了一个csp验证系统。实验表明,与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,在性质不满足时还可提供反例。