基于多元π演算的Web服务原子事务协议研究

Web服务事务协议放松了传统事务中的ACID属性的限制,重新定义了松耦合环境下事务性质,因此迫切需要对Web服务事务协议进行验证,以推进Web服务的工业化.采用多元π演算研究了Web服务事务协议形式化表达,详尽描述了WS-AT协议的两阶段提交协议2PCP,并定义了2PCP协议的原子性事务性质.最后,采用MWB工具证明了它的正确性.     

一种基于π t演算的安全协议建模方法

安全协议模型是安全协议分析与验证的基础,现有的建模方法中存在着一些缺点,如:建模复杂、重用性差等.为此提出了一种类型化的π演算:πt演算,并给出了相应类型推理规则和求值规则,πt演算的安全性也得到了证明.πt演算可以对安全协议、协议攻击者进行形式化建模.基于πt演算的安全协议模型及其建模过程使用NRL协议为例做出了说明.同时给出了攻击者模型,并证明了基于πt演算的安全协议攻击者模型与D-Y攻击者模型在行动能力上是一致的.这保证了基于πt演算的安全协议模型的验证结果的正确性.基于πt演算的建模方法能在协议数据语义、协议参与者知识方面实现细致的描述.与同类方法相比,该方法可提供多种分析支持,具有更好的易用性、重用性.分析表明,该方法可以在建模中发现一定的安全协议漏洞.     

ABC转运器的π-演算模型及其验证

将描述并行、分布式和可移动系统的进程代数应用于系统生物学的形式化描述和行为模拟,给出了SBP依赖式ABC转运器的π-演算模型,分析了其基于状态迁移规则的动态行为演变和构象变化过程,并用自动验证π-演算、通信系统演算CCS的移动工作台MWB对该模型进行了状态跟踪和性能验证. π-演算能够在统一的框架之下捕获分子生物系统的两个关键属性:模块化组织和动态行为,对其既能进行质的又能进行量的推理,证明了π-演算用于分子生物过程抽象描述的可行性.     

形式化多主体系统中的交互及交互协议

深入研究了多主体系统中的交互及其协议,并用一种进程演算;即π演算进行了形式化的描述.为了研究主体之间的交互,首先对参与交互的主体的行为进行了分类,并形式化地描述了其行为规范,然后用进程定义了主体间的交互协议,并在此基础上分析了主体交互的一致性及无死锁性.     

多实例工作流模式的π演算形式化

多实例工作流模式是一类重要的工作流模式。π演算是一种移动进程代数,可用于对并发和动态变化的系统进行建模。对π演算进行了研究，提出了以π演算作为工作流形式化的基础，利用π演算对多实例工作流模式进行了详细的描述。     

基于移动工作台的BPEL4WS死锁验证

描述了将Web服务业务流程执行语言(BPEL4WS)映射到π-演算的自动映射方法，对得到的π-演算表达式利用移动工作台（MWB）进行死锁验证，并给出一个具体示例。     

移动IPv6的快速切换的代数验证

利用π演算理论分析移动通信系统,可以严格而规范地描述其协议过程,并给予代数验证。文章基于π演算理论来分析移动IPv6的快速切换机制。首先建立了切换的π演算模型,然后通过推导,证明了模型的一致性。这将为移动IPv6的快速切换的研究提供一定的参考和分析价值。     

移动分布式实时事务实时原子提交

形式地给出了移动分布式实时事务实时原子提交协议的定义,在此基础上提出了适合于移动分布式实时事务的实时原子提交协议：一阶段实时原子提交协议(1PRACP)。1PRACP通过参与者与协调者的一次消息交换,在一个阶段完成移动分布式实时事务提交活动;结合超时恢复处理协议,1PRACP能避免由于站点故障或网络通信链路故障而导致的阻塞。对1PRACP进行了性能比较和评测,显示了它在各方面的优越性。     

分布式数据库两阶段提交协议研究与改进

分布式数据库具有可靠性和并行性等优点。在实现分布式数据库的过程中需要解决的最关键的问题是保证分布式事务的原子性、一致性、隔离性和持久性。两阶段提交协议可以解决这个问题,但是也存在一些缺陷。研究分布式数据库的事务处理机制,对基本两阶段提交协议所存在问题做了详细的分析并提出了一种两阶段提交协议的改进方案。     

一个带有时限的工程设计事务提交协议

通过分析协作设计活动的特点,给出了一个协作设计事务模型,并在此基础上提出了一个带有时限的工程设计事务两阶段提交协议,包括协议描述及故障处理。分析表明,带有时限的工程设计事务提交协议的性能在所有情况下优于基本两阶段提交协议。     

一种网格协同设计事务提交协议的研究

根据协同设计任务的特点,借鉴人们日常工作中协同设计项目的做法,提出一种网格协同设计环境下事务提交协议及其故障处理机制.该协议通过取消传统两阶段提交协议中的投票阶段,使参与者不必等待协调者的命令就可自行决定是提交还是终止.协议考虑任务的时限要求和质量要求,允许参与者自行决定是否参与协同设计,并允许参与者中途退出协同设计,从而放松了对事务的原子性要求.最后,从原子性、时限性、适应性等方面对提出的协议进行正确性证明;实验结果和性能分析验证了该协议的有效性和可行性.     

工作流模式的π演算形式化

为了实现工作流管理功能,必须将业务过程从现实世界中抽象出来,并用一种形式化方法对其进行描述.工作流模式是工作流建模的基本构造单元.π演算是一种移动进程代数,可用于对并发和动态变化的系统进行建模.首先提出以π演算作为工作流形式化的基础,然后利用π演算对工作流模式进行详细的描述.     

带有公平电子合同的交易协议

基于原子的公平匿名交易协议,采用两阶段提交的思想,通过可信第三方TTP(trusted third party)来控制交易的提交。在进行大量交易时,TTP会成为瓶颈。文中在原协议的基础上进行改进,引入了公平电子合同,改变交易提交方式,减少了TTP的工作量,但并没有破坏其原子性和公平匿名性,同时交易后产生的电子合同可具有传统交易合同的作用。     

带有公平电子合同的交易协议

基于原子的公平匿名交易协议,采用两阶段提交的思想,通过可信第三方TTP(trusted third party)来控制交易的提交.在进行大量交易时,TTP会成为瓶颈.文中在原协议的基础上进行改进,引入了公平电子合同,改变交易提交方式,减少了TTP的工作量,但并没有破坏其原子性和公平匿名性,同时交易后产生的电子合同可具有传统交易合同的作用.     

一种移动分布式实时事务原子提交协议

介绍了移动分布式实时事务的工作模式,在此基础上提出了应用于移动分布式实时事务的实时原子交换协议:两层实时原子提交协议.通过引入改进的TCP三次握手协议,完成移动终端与固定数据库系统的交互.对协议的正确性进行了证明.两层实时原子提交协议能够有效避免由于网络故障或者移动终端故障引起的通信堵塞.     

分布式数据库系统结点失败下无阻塞的提交协议

分布事务的原子性由分布事务的提交协议来保证。提交协议使公布事务在其执行结点上要么都一致地提交,要么都一致地夭折。如果一个分布事务的提交协议在系统失败时有可能致使某些分布事务的终止或继续运行依赖于此系统失败后的恢复,那么称此提交协议是有阻塞的。本文从提交协议的系统开销和阻塞程度两方面比较了目前常用的几种提交协议,描述了在结点失败下的无阻塞提交协议:带终止协议的三阶段提交协议。同时,本文还提出了在结点失败期间系统的处理策略,给出了保存失败给点悬挂动作以达到屏蔽结点失败的新方法。     

递归函数的π可定义性及其实现研究

并发计算模型是计算机科学研究的重要问题之一．π演算作为一个并发计算模型，是一种重要的移动进程演算，其中的进程通过发送通信链接互相交互．与传统的进程代数如CCS相比，π演算有着更为良好的代数性质和表达能力．正如λ演算能够描述所有的可计算函数，π演算也有同样的能力．本文提出了一个方法，据此可以把自然数和函数描述为进程，从而证明了π演算有足够的能力描述所有的可计算函数，同时还说明了与λ演算相比，π演算有着更高的计算效率．     

基于多Agent制造过程的建模方法

分析了制造系统与制造过程之间的关系;论证了从过程的角度对制造进行建模更恰当;结合Agent和π演算的特点,给出Agent制造系统描述模型及基于π演算的单个Agent的BDI模型,并指出Agent和π演算结舍的制造过程模型有利于进行优化目标在不同制造过程层次的分解,不论从方法的角度还是实现的角度,都适合复杂系统建模。Agent和π演算相结合可以有效分析并解决离散事件的建模与仿真中的问题。     

面向网格环境的事务提交协议的研究

提出一种面向网格的事务提交协议-ENP.该协议取消了两阶段提交(2PC)协议中的投票阶段,参与者无需向协调者发送COMMIT消息,可自行决定提交而不必等待协调者的COMMIT命令.如果参与者操作失败,则其向协调者发送abort消息后可自行终止,不必等待协调者发来的ABORT命令.性能分析和实验结果表明,该协议放松了对事务原子性的要求,可以降低提交协议的消息复杂度和日志复杂度,保证了网格环境中事务状态的一致性,满足了各参与者和资源的自治性要求.     

原子和公平匿名的电子交易协议的研究

基于公平盲签名技术、两阶段提交技术以及混合加密和数字签名技术,该文首次提出了一个能同时实现原子性和公平匿名性的电子交易协议。协议除了具有很好的原子性和匿名性外,对于非法的交易还提供了疑点追踪。文章详细描述了协议的工作过程,并分析了协议的原子性和匿名性。