论文部分内容阅读
面向服务的计算(Service Oriented Computing,简称SOC)为分布式计算提供了一种新的方式,在SOC模式下,一个任务通常需要不同服务的协作来完成,并且这样的协作经常需要第三方来实施。由于第三方不能够有效隔离服务的提供方,使得传统的ACID事务模型和两段协议并不适用于SOC中服务协作的场景。在此背景下,长事务中的一致性保证机制已经成为分布式环境下服务一致性保证的重要方法。为了确保长事务的正确性,现阶段提出了多种形式化语言来对长事务进行规约和验证,c CSP(Compensating Communication Sequential Process)是CSP语言面向长事务的扩展,而扩展c CSP在c CSP的基础上添加了进程并发、非确定性选择、递归、重命名、隐藏等建模功能,能够对分布式系统下的长事务进行有效建模。但是,当前扩展c CSP仅有指称语义,没有完整的操作语义。此外,到目前为止,扩展c CSP并没有相应的建模和验证工具支持。为此,本文研究了扩展c CSP的操作语义,以及扩展c CSP的模型检验问题,并基于操作语义实现了扩展c CSP的模型检验工具。本文的主要工作如下。基于已有的c CSP操作语义,提出了扩展c CSP的操作语义,解决了已有c CSP的语义规则不完备的问题,为每个扩展c CSP中的操作给出了语义规则。在此基础上,研究了失败发散语义与操作语义的关联关系,证明了两种语义模型的一致性。研究了扩展c CSP的正规性质验证问题的复杂性,通过将扩展c CSP正规性质验证问题归结到已知不可判定的Minsky 2-计数器停机问题,证明了问题的不可判定性。在操作语义的基础上,基于模型检验工具平台PAT(Process Analysis Toolkit)开发了面向扩展c CSP的建模与验证工具,支持扩展c CSP的建模、模拟及验证,其中验证包括线性时序逻辑(Linear Temporal Logic,简称LTL)模型检验,以及可达性、死锁、活锁、精化等关键性质的检查。使用了两个典型的长事务案例对语言和工具进行了展示,实验结果表明,工具能够有效支持各种不同类型性质的分析和验证,并且工具在时间和内存消耗上表现较好。