An exercise in structural congruence

Milner's structural congruence is decidable for the pi-calculus without restriction, in exponential space.     

Business process management—the third wave: business process modelling language (bpml) and its pi-calculus foundations

This paper introduces the ideas behind BPML, the business process modelling language published by BPMI. BPML provides a process-centric (as opposed to a datacentric) metalanguage and execution model for business systems. It is underpinned by a strong mathematical foundation, the pi-calculus. The current paper is derived from supplementary appendices to a book which describes a ‘third wave’ approach to business process management [Business Process Management: The Third Wave, 2003]. The aim is to model business processes directly in an executable form, so that the mobility and mutability inherent in business behaviour is reflected and supported in the corresponding IT systems, erasing the present IT-business divide.     

跨组织多业务事务建模与验证方法

面向服务的事务处理是保障业务交互和协作正确性的关键技术.针对跨组织多业务流程,提供了一种支持多业务事务建模与验证的方法.在建模方法上,对Pi-演算扩展了事务语义,将进程间的动作交互与跨组织膜活动相关联来刻画多业务事务协调行为.在验证过程中,基于等价自动机转换思路集成现有模型检验技术,验证多业务事务是否满足人们需要的各种性质.实验结果表明,该建模与验证方法能够有效地保障多业务流程在设计与实现过程中的正确性.     

面向跨组织业务流程的角色行为验证方法

为了更有效地保证跨组织业务流程模型的正确性和合理性,应用Pi演算提出了一种基于状态的角色行为的验证方法。基于Pi演算提出了跨组织业务协作中的角色模型,设计了角色描述表,以清晰、直观地描述角色的权利、职责和义务,进而应用Pi演算验证工具MWB(移动工作平台)的check和step命令提出了单角色验证方法,并在此基础上从业务对象状态和业务操作角度提出了多角色验证方法。实现了角色行为的验证,并为跨组织业务流程的可达性、一致性和死锁等分析奠定基础。     

多Web服务组合兼容性的自动化验证

Web服务组合的目的是实现单一服务无法满足的复杂功能,而保证组合的正确性以实现服务增值是十分必要,因此组合之后的正确性验证是Web服务组合的一个重要研究方向。从Web服务交互行为方面描述多Web服务组合,在提出行为兼容性的相关理论的基础上,给出基于Pi演算的多Web服务组合行为兼容性的自动化验证算法,通过将多Web服务组合自动转化为Pi演算中的组合进程,实现多Web服务组合的自动化验证。     

基于Pi-演算的工作流模式描述

工作流模式包含了业务流程的基本特征和共性,其实现依赖于具体的流程建模语言或方法.Pi-演算是一种进程代数,可以应用于业务流程的形式化建模.本文使用Pi-演算作为业务流程形式化的工具,对存在多种BPMN表示的工作流模式进行形式化建模,以探究工作流模式Pi-演算的描述,检验Pi-演算对业务流程行为特征的表现能力.     

Bisimulation verification using the up to techniques

This paper investigates the use of the so-called up to techniques for bisimulation in the framework of verification. We first introduce a method to exploit these techniques, that originate in theoretical works, in the applied context of verification. We then apply it on the π-calculus, in order to design an up to bisimulation verification algorithm for π-calculus terms. The outcome of such an effort is evaluated on two examples that were run on a prototype implementation. Published online: 18 July 2001     

基于Pi演算的构件行为兼容性研究*

构件行为的兼容性分析是研究构件动态交互过程中的重要问题,其研究结果可应用于构件替换、迁移、动态自适应演化等研究。为了保证构件在替换或组合之后系统仍能正常稳定运行,利用Pi演算对构件行为进行建模,并对多个构件行为间的兼容性进行验证,提出了绝对兼容、相对兼容等理论,并运用兼容度来判定构件行为兼容性强弱,且通过实例进行分析说明。     

Web服务相容性的形式化描述与分析

Web服务的相容性分析是为了保证多个Web服务之间的正确交互。基于Pi-演算对Web服务的相容性进行了形式化的分析,给出了二个Web服务之间相容性的两个形式化定义。同时定义了二个Web服务进程之间的投影操作,在此基础上给出了多个Web服务之间相容性的形式化定义。