一类新型的模块化高级Petri网--π-网

π-网是一类新型的模块化的高级Petri网．π-网有机地结合了两类并发模型Petri网和π-演算，π-网既可称为Petri网中的π-演算，又是π-演算的Petri网形式的体现，从而在语义上实现了从π-演算到Petri网的一种自动翻译，较完整地解决了π-演算的分布式语义问题．在π-网中，任一π-网都可由五类基本π-网：Tau网、输入网、自由输出网、受限输出网和匹配网通过π-网的复合规则复合而成，这一结果不仅使得一个π-进程能够在π-网中得到自动的演进，也使π-网自身具有了极大的可操作性和可计算性．     

基于π-演算的安全协议描述与验证

π-演算是以进程间移动通信为研究重点的并发理论，本文扼要叙述π-演算的基本概念，论述了如何用π-演算描述和验证安全协议，具体以Station-to-Station协议的一个不完全版本为例进行了分析，发现并在π-演算的工具MWB中证实了协议中存在的一个攻击，分析受到攻击的原因并给出了协议的改进版本．     

温控系统的π-演算的描述与验证

根据温控系统的特征以及需求说明,利用π-演算构建了该系统动态行为的交互模型,依据π-演算的反应规则仿真描述模型的行为交互过程,使用μ-演算和移动工作平台(MWB)工具分析和验证了该交互模型具有温度控制和阈值修改功能,从形式上证明了温控系统的需求说明及其π-演算模型的一致性。结果表明,π-演算能够清楚地描述和分析并发系统的行为交互,而μ-演算可以证明模型的有效性和正确性。     

基于时序可中断π演算的BPEL和BPEL4People建模

为了形式化地定义BPEL和BPEL4People的语义,提出了一个π演算的变种——πit演算。相对于传统的π演算,πit演算可以描述中断事件和时间事件,从而拥有更好的建模表达能力。介绍了πit演算的语法和语义,定义了一类强互模拟关系来判定πit演算进程间的行为等价,然后使用πit演算对BPEL和BPEL4People的活动进行了建模。该形式化模型有助于在BPEL和BPEL4People程序的设计阶段对其可靠性和一致性进行验证。     

Web服务事务的动态补偿模型

对π-演算进行扩展,提出了作为Web服务事务动态补偿模型的Exπ-演算.该演算的补偿可随着Web服务的交互动态地建立起来,同时给出了结构同余关系和操作语义.为了保证事务的唯一性,定义了一个简单的类型系统.最后,将该简化的Exπ模型与静态补偿模型和并行动态补偿模型进行比较,结果表明:本演算比其他演算更灵活,表达能力更强.     

Modeling BPEL and BPEL4People with a Timed Interruptable n-Calculus

为了形式化地定义BPEL和BPEL4People的语义,提出了一个π演算的变种——πit演算。相对于传统的π演算,πit演算可以描述中断事件和时间事件,从而拥有更好的建模表达能力。介绍了7ci。演算的语法和语义,定义了一类强互模拟关系来判定πit算进程间的行为等价,然后使用πit。演算对BPEL和BPEL4People的活动进行了建模。该形式化模型有助于在BPEL和BPEL4People程序的设计阶段对其可靠性和一致性进行验证。     

Combinator演算族的π演算语义

以SKI演算作为Combinator演算族的代表, 通过形式化的手段给出了SKI演算的π演算语义; 通过一个实例验证了所论方法的正确性. 所给出的转换方法证明了π演算的表达能力： π演算为图灵完备的. 由于高阶函数式语言与Combinator演算族之间存在着自然的转换, 所给的转换思想不仅为在π演算的理论框架下 研究Combinator演算族提供了基础, 也为探讨高阶函数式语言的表示和实现问题提供了新途径.     

网上拍卖系统的π演算建模

在分析了基于WEB的网上拍卖系统的需求基础上,针对具有多进程并发通讯特点的该类电子商务系统,采用π演算对系统进行结构和功能建模．本文在简单介绍π演算的语法和语义基础上,用进程表达式对整个系统软件结构框架进行了形式化描述,并分析了π演算的建模能力．结果表明π演算在描述动态进程间的通讯所表现出的优势以及便于编程实现的技术特点,尤其适合这类电子商务系统的分析与设计。     

用进程代数描述CORBA请求调用

用π演算模型来表现ＣＯＲＢＡ请求调用流程．对ＣＯＲＢＡ客户机和服务器端的主要部件（如：接口库、实现库、桩、对象适配器以及两端的ＯＲＢ等）在请求调用过程中的作用都用π演算进程加以表示．利用π演算对描述进程的并行性所具有的独特优势,通过对ＣＯＲＢＡ体系结构的高度简化,希望这一模型能够体现ＣＯＲＢＡ的高度并行和分布的特性．对动态和静态请求调用的分别描述,从理论上表现出它们的共性和区别．     

物联网服务的π-演算建模与验证

针对物联网服务建模和验证问题,用π-演算理论对物联网服务和环境实体进行动态交互行为建模,并引入μ-演算刻画物联网服务能力,将其描述为物联网服务和环境实体动态交互行为的执行序列。针对特定的应用场景,使用π-演算定义了物联网服务和环境实体,利用μ-演算对物联网服务能力进行建模,使用检测工具MWB验证了模型的安全性、活性和时间约束三个性质,为物联网服务建模和验证提供了参考。     

Email系统特征交互问题的π-演算检测

采用π-演算给出基于客户端-服务器模式的Email系统,以及系统中特征的行为描述;然后,利用μ-演算描述和分析Email系统中存在的特征交互问题.最后,利用移动工作台软件工具,验证基于π-演算描述的移动并发系统.     

用π-演算描述网络考试系统

在分析了基于W eb的网络考试系统需求的基础上,针对其具有多进程并发通讯的特点,采用π-演算对系统进行结构和功能的描述;在简单介绍π-演算的语法和操作语义的基础上,用进程表达式对整个系统进行形式化的描述;最后,通过实际编程实现,表明用π-演算描述这一类系统是非常适合的.     

动态软件体系结构建模方法研究

针对用现有方法对动态体系结构建模的不足，提出了一种软件体系结构抽象模型（SAAM）．sAAM以两种互为补充的形式化方法——面向对象Petri网OPN和π演算为语义基础，其中OPN可以形象地描述软件体系结构的初始化模型和动态行为，π演算可以描述软件体系结构的动态演化．这两种形式化方法通过SAAM集成在一起，并通过相应的支持工具对模型进行分析．在体系结构演化过程中，SAAM利用π演算的相关分析方法，对组件的演化策略和软件体系结构的一致性进行分析，从而可以在系统开发早期发现体系结构级的错误，提高软件质量．利用SAAM对经典实例自动加油站系统进行的建模与分析表明，SAAM直观、易懂，可以有效地刻画系统动态体系结构．     

扩展π演算对时间相关移动并发系统的建模与推演

针对π演算难于对时间相关移动并发系统进行建模和推演,提出了一种采用扩展π演算p-π对时间相关移动并发系统进行形式化建模与推演的方法。该方法首先采用区间动作前缀和瞬时动作前缀分别描述系统的时间相关行为和交互行为,并通过操作算子将子进程进行复合,然后利用操作规则构造出系统的时间相关标记迁移系统和可接受的执行路径,最后基于上述迁移系统和执行路径完成对系统性质的推演。对移动车辆控制系统的分析表明,所提方法可对时间相关移动并发系统进行有效建模和推演,保证时间相关移动并发系统的可靠性。     

CORBA/IOP的语义初探

用π－演算刻划ＣＯＲＢＡ／ＩＯＰ环境下涉及多个ＯＲＢ的分布式对象计算过程，重点描述多个ＯＲＢ之间的互操作过程．构造了一个高度简化的ＣＯＲＢＡ／ＩＯＰ的π－演算模型．借助于这个模型，演示了ＣＯＲＢＡ／ＩＯＰ支持分布式对象计算这个性质．     

一种有效的分布式构件交互性质验证方法

目的在基于构件的分布式系统开发过程中,更大程度地消除对构件交互风格和交互协议描述与验证产生的所谓的状态爆炸现象。方法提出一种有效的基于π-演算的构件交互协议验证方法——状态约减验证算法,在模型组合之前,将与性质定义无关的状态剥离,然后再进行模型组合。结果用标记转移系统证明了该验证算法的有效性,采用π-演算描述的同步请求/响应交互模型作为例证,证明上述算法比传统算法更有效。结论该算法缩小了组合模型的状态空间,提高了验证效率。     

并发计算的元模型Ⅴ.并发模型间的关系

讨论 pi演算和 chi演算之间的关系问题 .通过构造从 pi演算到 chi演算的翻译 ,证明了 chi演算的表达能力不亚于 pi演算 .该翻译保持操作性质和开互模拟等价的代数性质     

CORBA／IIOP的语义初探

用π－演算刻划ＣＯＲＢＡ／ＩＩＯＰ环境下涉及多个ＯＲＢ的分布式对象计算过程，重点描述多个ＯＲＢ之间的互操作过程，构造了一个高度简化的ＣＯＲＢＡ／ＩＩＯＰ的π演算模型，借助于这个模型，演示了ＣＯＲＢＡ／ＩＩＯＰ支持分布式对象计算这个性质。     

一新型移动进程模型—— χ-演算

提出一新型并发计算模型——χ－演算．它与π－演算的不同之处在于：具有统一的输入和输出，只有一类受限名，通讯的范围由局部化操作子界定，允许更大的并发度．着重研究χ－进程的代数性质     

一新型移动进程模型—x—演算

提出一新型并发计算模型－ｘ－演算，它与π－演算的不同之处在于；具有统一的输入和输出，只有一类受限名，通讯的范围由局部化操作作界定，允许更大的并发度。着重研究Ｘ－进程的代数性质。