通信顺序进程(Communicating SequentialProcesses,CSP)由Hoare于1978年提出,它是并发性研究的重要理论,是构建并发系统的经典方法。随着CSP在分布式系统、网络安全协议方面的应用,CSP的形式化验证显得尤为重要。目前,CSP的验证主要采用程序正确性证明和模型检测的方法。其中,程序正确性证明可以解决并发系统无穷序列验证问题,但采用手工证明或者半自动化证明的方法,且需领域专家的参与。模型检测是当前形式化验证的主流方法,可以自动完成并发系统的验证。本文对基于迹语义的CSP模型检测方法进行了探索与研究,并利用ASP(Answer Set Programming, ASP)技术实现了此验证系统。课题得到了国家自然科学基金(No.61262008)和广西可信软件重点实验室基金(KX201113)的支持。论文内容包括三部分:　　(1) CSP的新模型:min-trace模型。CSP的迹模型是一种数学模型,可在迹语义下对CSP进行具体的解释。它主要包括两方面的用途:一方面,为CSP语言的扩展提供正确性证明;另一方面,可以完成性质验证。通常 CSP的迹模型比较庞大,这为CSP的验证带来了困难。在迹模型的基础上,本文设计了一种min-trace模型。与迹模型相比,min-trace模型包含的数据量较小,可以减小模型转化时的计算量。此外,基于min-trace模型的性质验证是可靠的,因此可通过min-trace模型完成CSP模型的验证。　　(2)基于进程迹的CSP模型验证方法。当前,FDR(Failure Dviergence Refinement, FDR)是CSP模型检测的主流工具,它是在CSP的操作语义下将进程转化为相应的迁移系统,并通过迁移系统完成CSP的验证。FDR中性质采用迹进行规范,这不利于活性的描述;同时 CSP到迁移系统的转化比较复杂。为此,本文提出了一种基于进程迹的CSP验证框架,它在迹语义下生成CSP的min-trace模型,并通过min-trace模型完成性质的验证。与FDR不同的是,该框架中性质采用LTL进行规范,它的通用性更广,描述能力更强。　　(3) ASP技术在CSP模型验证中的应用。回答集程序设计(ASP)是一种面向复杂搜索问题的声明型程序设计方法,适合于解决知识密集型问题。本文利用 ASP构造了CSP的min-trace模型生成机制,并实现了一个CSP模型验证系统。与类似系统相比,该系统便于修改和扩展,描述能力更强,验证结果的准确性更高,在性质不满足时还可提供多条反例。