细胞膜演算：一种新的事务处理形式化方法研究

摘要

目前，Web服务逐渐普及，网格计算方兴未艾，移动无线网络逐步推广，在这些并发、分布和移动环境下，对事务处理的模型、语言和原型的研究正在展开.越来越多的电子商务和科学应用运行在异种平台上，应用程序之间相互通信采用基于消息的异步通信方式.如何协调各个应用之间的事务，以及如何保证这些协调的正确性，对事务处理的发展是一个十分关键的问题.以Web服务为例，提出了许多协议和模型：XLANG、BizTalk、WSFL、BTP、WS-AT/WS-BA、WS-CAF等，但大多没有做过形式化的表示和分析.图灵奖获得者TonyHoare认为，用形式化语义对事务进行研究，是“可达到的和有用的(accessibleanduseful)”，但目前没有普遍接受的描述事务处理的形式化方法. 本文提出了一种新的事务处理形式化方法-细胞膜演算(MembraneCalculus)，从语法、表达能力、操作语义、重写逻辑语义以及在事务处理中的应用等方面对其进行了研究.其主要内容如下： 本文定义了细胞膜演算的语法和操作语义.采用生物学细胞膜模型，扩展了提交Join演算中细胞膜的概念.细胞膜不但可以嵌套，用于表达位置和上下文的概念，本身可以移动、消失和生成，用于描述移动事务和动态变化的事务处理过程.在操作语义上扩展了一般进程代数所采用的化学抽象机模型，不但可以描述对象在细胞膜中的反应过程，可以描述动态嵌套细胞膜结构的演化过程.理论上证明了细胞膜演算能表达带抑制边的P/T网，从而获得与图灵机等价的表达能力. 本文给出了细胞膜演算形式化描述与模型检验(ModelChecking)统一框架-重写逻辑语义.本文定义了细胞膜演算重写逻辑语义，并结合重写逻辑定义了扩展细胞膜演算.采用重写逻辑工具Maude具体实现了细胞膜演算的重写模型MembraneCalculus.结合写逻辑中线性时序逻辑模型检验方法，提出了该演算的模型检验框架.通过重写逻辑()细胞膜演算将形式化描述和模型检验两者有机统一，改进了目前许多事务处()法只有描述没有验证的不足. 本文提出了移动事务和Web服务长事务的形式化描述与模型检验方法.文献上关于移动事务的形式化方面比较少，原因在于目前的形式化方法很难处理事务的移动以及本地事务与全局事务的协调.本文采用细胞膜演算，定义了哲学家问题的变体-移动哲学家问题的形式化描述，并且对其性质进行验证.针对文献中Web服务长事务经典例子，采用细胞膜演算定义了其形式化规范.运用Maude工具，得到其所有的状态空间，并采用线性时序逻辑对长事务正确性进行了分析. 本文分析了Web服务原子事务，获得其形式化描述并对其安全性和活性进行模型检验.本文没有局限于理论的探索上，采用细胞膜演算具体分析了当前比较主流的原子事务协调协议WS-AT.由于WS-AT协议采用简单的状态转换表和转换图，无法描述协调者和多个参与者的复杂协调活动.本文采用细胞膜演算给出了其形式化描述，用于规范协调者和参与者的活动，并分析了该协议的活性和安全性，得到了38187个状态，该协议满足稳定性、一致性和非平凡性，而不满足非阻塞性.并分析出注册和协调协议混在一起是其不满足非阻塞性的原因. 本文分析了Web服务业务事务，获得其形式化描述并对其安全性和活性进行模型检验.WS-BA协议是用于协调Web服务中业务事务的规范.本文采用细胞膜演算给出了该协议的形式化描述，定义了协调者和参与者的接口.在一个协调者和一个参与者情况下，该协议具有良好的性质，稳定性、一致性、非阻塞性和非平凡性均满足.但是在多参与者情况下，一致性不满足，这是该协议比较大的缺陷，原因在于WS-BA协议没有规定多参与者情况下的一致性输出协调策略.通过细胞膜演算，在实际应用中不但可以指出事务处理协调协议混淆和不规范的地方，而且可以分析协议的安全性和活性. 细胞膜演算是一个描述动态、移动的并发系统形式化方法，并不局限于事务处理方面.目前正在和西门子研究部门展开合作，研究如何将细胞膜演算应用于下一代可配置制造系统ReconfigurableManufacturingSystems(RMS)的流程执行模型的形式化描述和模型检验中.

目录

文摘

英文文摘

论文说明：上海交通大学学位论文答辩决议书

上海交通大学学位论文原创性声明及上海交通大学学位论文版权使用授权书

第一章 绪论

第二章 细胞膜演算

第三章 细胞膜演算重写逻辑语义

第四章 Web服务原子事务提交协议形式化描述与模型检验

第五章 Web服务业务事务协调协议形式化描述与模型检验

第六章结语

参考文献

附录1WS-AT协议状态转换表

附录2WS-AT细胞膜演算形式化描述

附录3WS-BA协议状态转换表

附录4WS-BA细胞膜演算形式化描述

致谢

攻读学位期间发表的学术论文目录（第一作者）