着色Petri网的结构展开方法

为提升着色Petri网的设计分析与模型检验能力,讨论了着色Petri网的结构化展开技术.以着色Petri网的令牌单元和绑定单元为基元,通过对着色Petri网展开为普通Petri网的等价性证明,提出了基于着色Petri网关联矩阵和标准元语言的展开规则和规范化步骤.研究结果为着色Petri网到普通Petri网的自动转换过程和着色Petri网验证提供了有力支持.     

一种高可用异构容错系统的混合可用性模型

为解决高可用异构容错系统的可用性评价问题,提出了一种针对高可用异构容错系统的混合可用性评价模型。设计实现异构容错原型系统,包括硬件体系结构框架及软件系统。采用Markov过程与随机Petri网相结合的方式,从可用性量化和系统状态转换两方面构建系统的可用性模型。根据该可用性模型估算系统的高可用指标,并与同构及非容错单机系统进行比较分析。结果表明,该可用性模型能够对异构容错系统进行准确的可用性评价,验证了系统5个9的高可用指标要求。最后总结了影响系统高可用性的主要因素及提升系统可用性的有效方法。     

一种验证软件演化过程行为的代数推导方法

针对现有软件过程验证主要以结构验证和性质验证为主,缺乏行为验证的不足,提出了一种验证软件演化过程行为的代数方法.该方法使用通信进程代数ACP对软件演化过程元模型EPMM进行扩展,提出软件演化过程元模型代数EPMM-A.针对EPMM建模产生的软件演化过程模型,一方面使用EPMM-A形式定义软件演化过程模型的行为规约,另一方面在其公理系统的支持下,基于等式推导验证软件演化过程模型的行为与行为规约是否一致,使行为验证方式从模型推导(非形式化)变为代数推导(形式化).为了说明代数推导的正确性,证明了软件演化过程元模型代数的公理系统具有可靠性.     

ASBS适应行为稳定性分析

研究了基于服务的自适应软件系统的适应策略构建中适应行为的稳定性分析问题.主要采用了基于反射Petri网模型的分析方法,在反射Petri网模型中系统的业务行为与适应行为在不同的层次分离建模,适应行为模型相对业务行为模型透明.结合系统的反射Petri网模型提出了适应行为稳定性的具体定义,给出了适应策略中适应规则的建模方法以及应用反射Petri网模型对系统适应行为进行稳定性验证的方法,并通过一个实例对方法的可行性以及有效性进行了说明.     

井下机车运输调度的资源分配模型及无死锁优化调度

对井下机车运输系统进行无死锁调度和性能优化, 首先, 建立三种不同调度策略下的资源分配Petri网模型, 设计对应调度策略下无死锁标识的最大边界设置算法, 证明了调度策略在最大标识边界设置下的无死锁性. 然后, 以最小化时耗和能耗为优化目标, 利用遗传算法, 采用变迁标号的自然编码方式, 通过检查变迁的引发条件检测染色体的可行性, 修复不可行的染色体使其对应的调度满足资源约束, 从而保证了算法所利用的所有染色体均可对应系统的可行调度, 最后进行实例仿真. 设计的无死锁调度的最大标识边界设置算法和遗传算法为井下机车的运输调度提供了可靠的理论基础.     

制造过程不确定质量异常诊断的Stateflow方法

模糊推理Petri网可以对制造过程不确定质量异常诊断进行有效建模, 但其复杂的图形表示及模糊推理逻辑结构使模型难于进行仿真分析. 通过建立模糊推理规则与Stateflow元素之间的映射关系, 将模糊推理Petri网模型转换为便于仿真的Stateflow模型, 模型以质量控制图异常模式数据作为输入, 实现不确定质量异常诊断过程的动态展示. 某工件加工过程不确定质量异常诊断的仿真结果表明, 模型可以输出引发控制图实时异常的异常原因的贡献度, 为异常消除提供决策支持.     

基于Petri网的敏捷制造业务过程建模研究

在分析敏捷制造业务过程的基础上,给出了该业务过程的Petri网系统描述,并提出了Petri网过程模型.该模型描述了敏捷制造中多因素相互间的动态行为,解决了其过程中各环节之间的并发性、异步性、分布性等问题.最后,运用可达树分析方法分析了网模型的活性.     

基于随机文法的骨架结构化表示

针对传统目标骨架多采用图结构表示存在的缺陷,基于描述随机模式的随机文法技术,提出了用随机文法表示目标骨架,其核心是利用随机文法的抗干扰能力解决骨架对噪声的敏感,在随机文法中嵌入骨架权值抓住目标主要的拓扑特征,与传统的图结构对比,它能提高骨架的抗干扰能力,防止目标主要形状的丢失。     

Soundness analysis of compositional model of time-based petri nets

Workflow management systems are widely used in improving the efficiency of business processes.To develop a workflow management system is the key to workflow modeling.In this paper,the compositional time net is presented to model workflow processes on the basis of the analyzing methods of time Petri nets and workflows,and to describe the static relationships and the dynamic semantics of the task of multiple workflow composition.The paper puts more emphasis on checking the soundness of composed workflow,at the same time,combinational problems of non-conditional structure of the compositional time net are introduced and analyzed.A sufficient and necessary condition for determining the soundness of compositional nets is obtained.     

基于扩展ITCPN的UML状态图建模

在ITCPN（IntervalTimedColoredPetriNets）模型的基础上引入变迁条件函数和变迁数据操作函数,实现对UML状态图中数据计算的建模;利用抑止孤对迁移的优先级进行建模;同时借助抑止弧实现了对UML状态图中子状态之间“或”语义的建模。