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

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

基于π网的多Agent系统建模与分析

首先集成两种互为补充的形式化方法-面向对象Petri网(Object-Oriented Petri nets,OPN)和π演算,建立了一种通用的形式化建模方法——π网.π网利用OPN形象地描述系统的初始化模型及动态行为,利用π演算刻画系统的动态演化.然后以π网为语义基础,从软件体系结构的角度,建立了一种多Agent系统体系结构模型(Multi-agent Systems Architecture Model,MASAM).在MASAM中,将多Agent系统抽象为计算Agent、连接Agent和配置等三个单元,并描述了多Agent系统的动态演化;研究了系统演化后体系结构一致性的分析方法,从而可以检测系统开发早期存在的错误,确保模型的可靠性和正确性.     

多Agent系统形式化建模方法研究

简要总结了多Agent系统（MAS）形式化建模方法的研究现状;以面向对象Petri网（OPN）和π演算为基础,给出了一种直观的MAS体系结构模型（Multi-Agent Systems Architecture Model,MASAM）。OPN可以形象地描述MAS的初始化结构及动态行为,而π演算可以刻画MAS的动态演化;另外,可以利用Petri网和π演算的相关分析方法和支持工具分析和验证系统模型,在系统开发早期发现并避免体系结构级的错误。     

基于π演算的自治系统架构描述语言AS-ADL

自治系统(Autonomous Systems)具有复杂的动态结构和行为特性,其典型代表就是各类军事作战系统.针对当前各种自治系统架构描述方法存在的局限,建立了自治系统架构的概余模型框架,并提出了一种描述该模型框架的形式化架构描述语言AS-ADL.AS-ADL以高阶多型π演算作为系统行为语义基础,具有丰富的数据类型,可以形式化描述自治系统的动态行为,且具有描述自治元素内部的交互行为的能力,为建立可执行的系统架构模型奠定了基础,并为系统模型求精和模型有效性验证提供支持.     

密码协议的π -网形式化描述和分析

π-网是一类模块化的、具有代数演算功能的高级Petri网.通过引入项、buffer库所和解密变迁等建模元素,本文在π-网中建立了密钥管理和加密信息的传输机制,形成了密码协议的Petri网形式化模型,而且对于任意的一个密码协议,都可以将其模块化,本文还提出了密码协议的鉴别性和安全性的验证机制.通过对Needham-Schroeder协议的实例分析,对密码协议的密钥交换和鉴别性,以及协议存在的漏洞,进行了有效的形式化描述和分析.     

信息物理融合系统可信软件形式化建模与分析

从多Agent系统的角度,以Petri网和π演算为语义基础,建立了一种信息物理融合系统（cyber-physical systems,CPS）可信软件形式化模型（high-confidence software formal model,HCSFM）. HCSFM以Petri网形象地描述CPS可信软件静态结构模型及动态行为,用Petri网分析方法和支持工具对模型进行分析和验证; 利用π演算刻画CPS可信软件中Agent的加入、退出、更新和体系结构重配置等动态演化机制,并研究Agent的演化策略及演化后CPS的一致性,确保动态演化后CPS软件能正常交互,从而为CPS软件设计提供可信保障. 通过HCSFM在无人驾驶车辆编队CPS中的应用,表明HCSFM可以有效地对CPS可信软件进行建模和分析.     

基于封箱演算的形式化组织模型

组织是群体对抗的主要形式.一个好的组织模型有利于提高规划识别的精度和效率.封箱(seal)演算是π-演算的变体.将封箱演算引入动态联盟组织模型建模中,为组织模型的形式化研究提供新的手段.利用封箱演算工具,给出了形式化组织模型,提出了一种基于角色的层次性组织生成方法,并讨论了由于角色变化带来的组织动态调整.     

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

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

基于Pi-演算的信任网络形式化建模

网格环境下实体信任网络的形式化建模是实现其仿真的关键环节,利用pi-演算刻画网格中信任网络的结构和交互。抽象定义信任网络,讨论信任网络节点与Pi-演算的对应关系,给出基于Pi-演算的信任网络建模规则和建模过程,借助pi-演算模型检测工具对提出的信任网络形式化系统进行行为分析与推演,结果表明其具有活性和安全性,且能有效满足用户在信任方面的服务质量需求。     

面向组合的业务流程建模及异常处理

随着信息技术的发展，业务流程的范围扩展至跨越部门，甚至跨越企业的边界，复杂性也越来越高。提出一种形式化的面向组合的业务流程模型，该模型以流程代数π演算为形式化基础，通过组合简单的结构化流程控制模块，建立复杂的流程模型，并给出了模型的合理性验证。利用流程可组合的特性，将异常处理逻辑从正常的流程控制逻辑中分离出来，并将异常处理区域化，以最小化计划外偶然事件的有害影响。     

不可否认协议形式化分析的Petri网方法

Petri网是一种描述及分析并发行为的工具,在安全协议的形式化分析中得到了广泛的应用,但目前还没有人使用Petri网来分析不可否认协议.本文以一般安全协议的Petri网分析方法为基础,提出了使用Petri网分析不可否认协议的建模及分析方法,该方法可以描述并分析一些其它形式化方法无法描述的协议性质.使用该方法分析J. Zhou和D. Gollmann的公平不可否认协议发现了它议的一个许多其它形式化方法不能发现的已知缺陷.     

A New Signal Processing Technique of π/4-DQPSK Modem Based on Software Radio

1 .INTRODUCTIONπ/4 DQPSKmodemhasbeenchosenasthemodemschemeinmanymobilecommunicationsystems[1 ] .Inπ/4 DQPSKmodem ,theinformationbitsaremappedintophasetransitionsratherthanabsolutephasevalues.Thisencodingofinformationinthetransitionsovercomesthephaseambiguityproblemsresultingfromtheestimationofcarrierphaseinnon differentialPSKsystems.Soπ/4 DQPSKallowsforsimplebasebanddifferentialdemodulation .Further,inπ/4 DQPSK ,themaximumphaseshiftisrestrict edto± 1 35°(ascomparedto± 1 80…     

C4ISR系统能力需求行为建模及验证

针对C⁴ISR系统需求分析行为建模中,统一建模语言（unified modeling language, UML)的行为模型验证困难问题,提出了一种C⁴ISR系统能力需求行为建模及验证方法。从构建C⁴ISR能力元概念模型入手,通过扩展UML行为元模型得到能力行为元模型,然后使用能力行为元模型来构建能力需求的行为模型。为了检查行为模型是否满足能力元概念模型、能力行为元模型和领域规则约束等模型一致性和领域完整性问题,将行为模型的语义形式化为OWL-DL和DL-Safe规则表示的本体,并定义模型检查规则通过对本体进行逻辑推理和查询实现模型验证。     

混合系统及其建模

在概述混合系统概念、特点、发展近况以及混合系统框架的基础上，介绍了混合系统研究中的建模问题，重点介绍了等价离散事件模型、混合自动机、Petri网、时段演算及其扩展等建模方法，最后介绍了混合系统研究中的一些重要成果以及一些仿真方法。     

一种基于MDE的形式化组合建模仿真方法

大规模的联合建模与仿真迫切需要提高模型及仿真的可组合性.针对实现可组合仿真的主要问题,分析并提出了基于不同抽象程度的组合仿真的层次化功能结构模型.结合MDE模型驱动工程的设计思想,应用形式化建模的相关方法和π语言,提出了覆盖可组合仿真系统设计整个生命周期的一整套开发方法.同时,建立了基于MDE的模型映射机制,实现了基于一系列工具支持的不同模型之间的相互关联和转换,并在某大型分布式仿真系统开发中得到了应用.     

基于Petri网模型检验的安全关键软件需求验证

需求形式化建模和模型检验可以提高安全关键软件的可信性,但在模型描述、调试和解释能力方面存在局限。对使用Petri网支持软件系统建模进行了扩展,设定默认值为零的权函数、利用“非”虚线描述在状态为假和变迁失败情况下的触发,增强阈值条件的描述能力,区分了枚举型和数值型库所,区分了普通迁移和强赋值迁移,并给出了扩展后的形式化定义及其和检验语言的语义映射。最后给出在典型机载软件上的应用,建立了软件需求模型和部分映射代码,对模型进行检验、反例路径分析和需求完善。过程和结果表明该方法可以有效的支持实际的关键安全软件需求建模和验证。     

基于CPN的联邦概念模型形式化建模与验证(英文)

提出了基于着色Petri网(CPN)的联邦概念模型(FCM)形式化建模与验证一体化方法。这种方法的提出主要基于下面两点:一是形式化的FCM与用自然语言描述的模型相比具有更完整、更准确和更规范的特点;二是形式化模型的验证需要专门的工具辅助完成。以一个简单的制造系统为例,采用CPN语言建立了该系统的形式化概念模型,利用辅助软件工具CPN Tools完成了该联邦概念模型的仿真和验证。应用研究表明,着色Petri网有助于描述联邦中各实体的行为和关系,CPN Tools辅助工具实现了形式化模型建模、仿真和验证的一体化过程。     

面向体系仿真的指挥控制网络行为建模研究

合理有效地对指挥控制网络行为进行建模是体系仿真的关键。通过分析EBI框架下实体行为建模的层次,提出了一种适用于刻画具有复杂适应性特征的指挥控制网络行为的层次建模方法。首先,提出了采用UML时序图和流程图对任务和任务阶段建模。其次,提出了基于ECA规则的动作建模方法,提出了内部动作和外部动作的定义,根据经验给出了化简动作关系图的规则,并给出了动作的形式化描述。最后,给出了防空体系指挥控制网络行为建模的应用实例,验证了该方法结构合理、层次清晰并具有一定得扩展性。     

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

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

无人蜂群电磁作战行动建模与仿真

针对自主、协同、智能的无人蜂群电磁作战行动难以描述、刻画、建模与仿真的问题,首先以联合作战为背景,分析了无人蜂群电磁作战行动的层次化特征,并基于BNF (Backus-Naur form)描述了作战行动链。随后,分析了无人蜂群个体自主作战与群体协同作战的行为特征,并以此为基础提出了基于RRA (rule, respond and algorithm)的无人蜂群电磁作战行为模型建模方法,给出建模具体流程与行为规则的形式化描述。再次,构建了个体电磁辐射源目标自主识别行为模型,以及群体电磁攻击协同目标分配行为模型,完成了RRA方法的具体实现。最后,通过作战仿真实验与算法验证实验,证明了本文建模思路与建模方法的合理性、有效性。