论文部分内容阅读
计算机网络已经渗入到人们生活的各个领域,微小的错误可能导致无法挽回的损失甚至危及人的生命。通信协议是网络正常发挥作用的基础,如何保证它的可靠性和安全性是学术界和工业界均非常关注的一个重大问题。CSP(Communicating Sequential Processes)是一种经典的建模语言,它能够充分描述协议的并发性。因此,通信协议的CSP模型性质验证是一项具有理论和实际意义的研究课题。目前,CSP模型的验证方法有定理证明和模型检测。定理证明能够处理无限状态序列问题,但需要专家参与。模型检测是验证CSP模型的主流方法,拥有众多模型检测工具且能够自动完成。但现存的检测工具是在操作语义下将进程转化为迁移系统进行验证,转换过程较为繁琐且不易修改和扩展;LTL(Linear Temporal Logic)是描述性质的通用语言,但是除PAT外,CSP模型检测器都使用迹描述性质,不利于活性等的验证。 本文研究基于ASP(Answer Set Programming)技术的通信协议CSP模型性质验证,构建了基于ASP的通信协议CSP模型验证框架,建立了CSP进程和LTL公式的ASP描述形式及开发了相应的自动转换工具,改进了基于ASP的min_trace模型生成技术,提出了通信进程的并发组合方法。开发出CSP模型检测器C_ASP。 详细地,本文主要研究成果如下: (1)构建了基于ASP的通信协议CSP模型验证框架。比较了文献中基于ASP的并发系统CSP模型验证框架的优点和不足,建立了基于ASP的通信协议CSP模型性质验证框架,给出了本文框架下的验证流程,并以AB协议为例进行说明。 (2)提出了CSP协议模型和LTL公式到ASP程序的转换技术。建立了CSP进程的ASP谓词形式,其中CSP进程由前缀、递归、事件选择、非确定性选择、一般选择、顺序、赋值、条件分支或并发9种算子构成。给出了基于ASP的min_trace模型生成技术,提出了通信进程基于 min_trace模型的并发组合技术。给出了 LTL公式到ASP程序的转换,其中LTL公式包含原子p和?、∧、∨、G、X、F等连接词。 (3)开发了CSP模型验证工具C_ASP。给出了C_ASP的算法,该算法包括调用CSPtoASP和LTLtoASP转换器,并开发出相应的工具,其中,CSPtoASP和LTLtoASP实现了CSP模型和LTL公式到ASP程序的自动化转换。C_ASP实现了输入 CSP模型和 LTL公式立刻输出结果,且能够一次运行验证多条性质。AB(Alternating Bit Protocol)协议的实验结果表明本文验证框架及开发工具 C_ASP的正确性和高效性。