同步和异步π演算的表达能力研究

以π演算为框架,通过研究同步和异步通信机制,澄清了各个算子对语言表达能力的影响.给出了一个编码,它以同步π演算作为编码的源语言,异步π演算作为对应的目标语言,在同步π演算中保留match算子、全复制算子、并行算子和受限算子以及输入输出前缀,而异步π演算保留lazy复制算子、并行算子、受限算子、输入前缀以及没有后继的输出消息.研究结果证明了编码在接口互模拟关系下是完全抽象的,从而证明了编码的正确性.进一步说明了在不考虑不确定选择算子的情况下同步通信机制和异步通信机制的等价性,并为π演算的实现提供了理论依据.

基于π演算的指挥决策行为形式化建模研究

指挥决策行为建模研究急需能够为分析、描述和建模指挥决策行为所具有的并发性、复杂交互性以及动态演化性提供有力支持的形式化方法。基于改进的OODA,通过应用π演算对指挥决策行为进行形式化建模,探讨了基于π演算的指挥决策行为形式化建模的可行性和可用性;在此基础上,就π演算方法为指挥决策行为形式化建模正确性验证以及模型有效性验证方面所提供的支持进行了初步探讨。研究表明,π演算方法可为指挥决策行为建模提供有力支持。

基于π演算的软件人群体形式化建模

在参考多智体系统的基础上,根据大系统控制论的分解协调思想,提出一种软件人群体体系结构,并对其关键技术如本体库、知识库、任务库、通信协议、角色模型、交互模型等进行了描述.描述了对该系统从分析到设计的整个构建过程,并采用π演算形式化方法对整个系统的信息流和控制流,以及任务之间的4种协作方式进行了建模.对于不同的应用领域,通过定义相应领域的本体库和所需的角色以及任务分解,即可快速构建相应的应用系统,为分布式系统提供了一种解决方案.

基于高阶时间π演算的构件式实时软件研究

在复杂的实时软件系统中使用构件式设计方法已成为目前软件工程中的研究热点。如何有效地验证实时软件的设计是否满足给定的时间规约,是实时计算领域中的主要挑战之一。文中提出了一种有时间特性的高阶多型π演算(THOπ-calculus),通过对不同阶上进程中活动关联的持续时间和最晚结束时间加以约束,给出了THO-π演算的操作语义。作为对π演算模型等价性分析的重要工具,在THO-π演算语义下提出了一种新的弱时间互模拟关系,并针对弱时间互模拟关系的阶次性定义了多分辨时间约束。通过对某导航软件的设计表明,该方法对实时软件构件内部、构件间的复杂动态时间约束有很好的表达与化简作用。

工作流模式的π演算建模研究

π演算是一种移动进程代数,可用于对并发和动态变化的系统进行建模。根据π演算的语法,提出了一种新的用于工作流模式的形式化建模方法,以π演算作为工作流形式化的基础,并利用π演算对工作流模式进行了建模。

π演算的Petri网语义研究

为弥补π演算的固有缺陷,提出一种将π演算映射为Petri网语义的方法.该方法将π演算分为基本单元、顺序、并发、选择和递归等几种基本结构,分别映射为Petri网,然后复合构成复杂的系统.π演算的Petri网语义可形象地描述系统的物理结构和动态行为,可直接从模型网络结构上定性分析系统的性质.最后,利用该方法将移动汽车网络的π演算模型映射为Petri网,验证了方法的有效性.

基于π演算的工作流模型分析方法

使用合理性、弱合理性和松合理性对π演算形式化的工作流模式进行合理性分析时,工作流都不符合这3种合理性。针对以上问题,提出懒惰合理性的概念,用于对工作流进行分析。通过考虑节点语义,扩展结构合理性。为了表达节点语义,用π演算表达过程图,使过程图具有形式化语义。

基于π演算的舰船作战任务流程建模

针对舰船作战任务流程仿真和任务成功性研究的需求,运用π演算理论,对舰船作战任务进行了元任务分解,确定了执行命令-条件-运行设备(command-condition-equipment,CCE)规则。在此基础上,研究了一种基于元任务的作战流程π演算形式化和基于CCE规则的元任务建模方法。利用该方法对潜艇鱼雷攻击过程进行了建模,并分析了任务过程的复杂并发性、不确定性和动态演化性。最后,使用MWB工具对所建模型进行了验证和推演,证明了该模型的正确性和有效性,为舰船作战任务流程建模和分析提供了一种新的技术途径。

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

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

基于π演算的反射式需求规约描述方法

目前,大多数学者都意识到需求演化的重要性,然而依然缺乏有效的方法指导需求演化。反射式需求规约通过描述支持OWL-S需求规约演化的元信息,并支持以合理的方式使用这些元信息,实现OWL-S需求规约的演化。本文提出了一种基于π演算的反射式需求规约演化模型,使得反射式需求规约的演化能够以一种正确的方式实现。针对OWL-S需求规约的特点,给出了OWL-S需求规约的π演算描述方法;使用高阶π演算的进程传递机制,描述了支持演化的反射式需求规约;给出了反射式需求规约演化正确性的推理与验证方法。同时,我们采用交通出行的例子论证了本文的观点。

基于π演算的动态软件架构研究

动态软件架构(Dynamic Software Architecture)是架构领域的研究热点。分析了动态软件架构建模应关注的问题,基于π演算提出了动态软件架构形式化建模的方法,给出了动态软件架构语义的推导算法,奠定了动态架构行为分析和仿真的基础,并能对动态架构的诸多要素进行建模,包括动态演化的起因、时间、操作、非瞬时特性、断点继续执行等。

基于应用π演算的可信平台模块的安全性形式化分析

可信平台模块(trusted platform module,TPM)是信息安全领域热点研究方向可信计算的关键部件,其安全性直接影响整个可信计算平台的安全性,需要对其进行安全性验证.针对已有工作对TPM规范中多类安全性问题进行形式化建模与验证过程中所存在的不足,从分析TPM和使用者的交互过程出发,使用应用π演算对TPM进行形式化建模,把TPM规范中定义的各实体行为特性抽象成为进程的并发安全性问题,在讨论并发进程中机密性、认证性和弱机密性的基础上,对交互模型进行安全性论证,提出并使用自动定理证明工具验证了对应安全属性的改进方案.

基于π演算的一种Agent组织模型

Agent组织是多Agent系统研究的重要方面 从直观含义出发 ,将组织看做Agent之间的控制关系 ,以π演算为工具 ,给出了组织角色的定义和根据组织框架构建具体组织的过程 角色和组织框架都用进程表示 ,确定了Agent加入和脱离组织的严格描述 相比Ferber等以π演算和化学自动机定义组织形成过程的形式语义的工作 ,本文显式定义了角色和组织框架 。

基于π演算的攻击编队组织的动态演化

根据空战作战任务的特点,对协同攻击任务进行阶段分解和类型分解。建立了基于任务、面向结构、具有集中-分布式指挥控制关系的作战编队组织结构。应用π演算对编队成员的任务角色的指派、维持、更改和角色冲突协调等编队组织动态演化问题进行了研究,使编队成员任务角色可根据空战态势、空战任务和编队成员的生存力等进行及时调整,确保编队有效的实施对目标的协同攻击。

基于高阶多型π演算的可生存系统认知模型研究

提出一个具有多层感知能力的可生存系统认知模型。基于高阶多型π演算把认知模型的形式化建模与认知能力的量化分析同步结合,通过对系统运行状态和系统业务及内部结构形式化建模后进行认知能力的量化评估。提出一个具有多层感知能力的可生存系统认知模型;基于高阶多型π演算对可生存系统认知模型从两个角度进行形式化建模;利用MWB工具实现对不同攻击场景下的系统可用性、瞬时可用性、稳态可用性和高优先级任务吞吐量的试验。

基于L-π演算的WSN路由协议形式化方法

针对无线传感器网络路由协议形式化描述与验证的问题,提出了一种形式化方法 L-π演算。定义了L-π演算的语法,形式化描述无线传感器节点的广播与单播的通信行为。定义了相应的结构同余,描述了节点表达式的非顺序性。定义了相应的迁移规则,提供了路由协议形式化模型的动态推演功能。通过对无线传感器网络簇头选择协议的描述展现了L-π演算的能力。通过无线传感器网络簇头选择协议的验证实验说明了该方法能有效验证无线传感网络路由协议。

为π演算建立具有安全级别的简单类型系统(英文)

为π演算建立具有安全级别的简单类型系统,并证明该类型系统在规约语义下的类型可靠性.此类型系统使得π演算成为安全系统、安全协议分析与规范的普适形式化工具.

基于π演算的云服务安全检测

利用π演算对云服务流程进行形式化描述,基于描述结果给出一种针对用户越权访问和服务不完整两种安全性问题的检测方法.基于云环境下的虚拟机部署实例对该方法的流程进行了说明,并将该方法与Bayes网和预测规则集等安全检测方法进行对比.结果表明,该方法能同时保证云服务过程的一致性和安全性.

带π演算验证的FMIPv6优化方案

为解决FMIPv6的切换延迟长和丢包率高的问题,提出一种改进方案PI-FMIPv6。该方案通过引入信息学习机制、绑定代理机制及隧道定时器,将转交地址配置、重复地址检测、绑定注册等工作提前完成,并合理设置隧道生存期,优化了FMIPv6切换流程。通过π演算对PI-FMIPv6方案进行数学模型定义和推导,证明了PI-FMIPv6方案的规范性和严谨性。同时,NS-2仿真结果表明,改进方案PI-FMIPv6相对原FMIPv6方案减少至少60.7%的切换延迟和61.5%的丢包率,验证了其性能优于FMIPv6,更好地满足了实时业务的需求。

基于π演算的多实例工作流模式的建模方法

π演算是一种移动进程代数,可用于对并发和动态变化的系统进行建模。根据π演算的语法,利用π演算对多实例工作流模式进行了建模。提出的方法具有较强的语义表达能力,同时使过程模型的语义更加精确。