基于扩展混成Petri网的CPS无人车系统建模与分析

信息物理融合系统(Cyber-Physical System,CPS)是一个集计算系统、通信系统、感知系统、控制系统和物理系统于一体的复杂系统,其行为是一种由离散计算过程与连续物理过程深度融合并紧密交互的混成行为。针对这种特性,采用混成Petri网对CPS建模,并在此基础上添加时间约束,即对离散变迁关联一个延迟时间,对连续变迁关联一个激发速率函数,同时引入抑止弧和测试弧的概念以提高Petri网的表达能力,由此提出一种新的模型——扩展混成Petri网模型。然后,对CPS应用中无人驾驶车辆系统的躲避障碍物场景进行建模,将建立的模型按照一定的规则转化为与之对应的Simulink模型,并通过Matlab仿真对系统行为及属性进行分析。     

穿刺机器人运动安全性的形式化分析与建模

混成系统是实时嵌入式系统的重要子类,其行为中存在连续变化和离散跳转混杂的情况,使得混成系统行为复杂,安全性难以掌握。近年来,混成系统在医疗环境中得到越来越广泛的应用。其中,医疗机器人的穿刺运动控制系统呈现高度复杂的混成性,如果机器人在穿刺过程中失控将导致不可挽回的严重后果。因此穿刺机器人运动行为的安全性设计成为了亟需解决的问题。首先根据穿刺机器人的运动学设计,将机器人的复杂运动分解。然后基于微分动态逻辑理论从混成系统的角度出发对穿刺机器人的运动控制系统进行了形式化建模与分析,并使用证明工具KeYmaera归纳出微分不变式,获得了控制模型的参数约束。最后提出了针对机器人运动到某一靶目标区域这类运动学问题的一般性验证模型。     

基于扩展DPN的CPS混成行为时效建模与综合评估

信息物理融合系统行为是一种由离散计算过程与连续物理动态过程深度融合并紧密交互的混成行为.在CPS设计早期对信息系统实体的信息实体的关键监控参数、实时指标,以及物理系统设施的连续行为规律进行综合评估,是这类系统进一步设计与实现的基础.基于扩展DPN语义,以某智能车CPS系统自主行进紧急避障过程为研究对象,建立了其信息物理混成行为的Petri网模型,以融合并集中体现各关键参数和指标的时序协作效应;通过对该模型的仿真运行,实现了CPS行为的在线观测与综合评估.该方法为CPS子系统关键设计指标的综合合理性评估及其组合设计提供了一种解决途径.     

静态混成自动电压控制的研究

将混成控制系统理念引入电力系统的静态电压控制,提出了静态混成自动电压控制系统.首先,建立了分层分级的静态电压控制系统模型并设计了系统运行流程.其次,定义了安全性事件和经济性事件的发生机制,利用离散事件驱动高层控制,形成的控制目标再下发至各对应的控制模块,从而实现复合指标控制,该系统降低了优化问题求解难度,提高了运算效率,具有较高的可实现性.而且,该控制系统充分适应电力系统连续-离散相耦合的特点,协调各种电压控制设备.计算机仿真研究表明,该控制系统可以提高电网的电压安全性和电压质量,合理分配无功,同时减少网络损耗.     

多机器人路径规划的安全性验证

近些年来,伴随着人工智能领域的浪潮,机器人越来越多的出现在我们的日常生活中,例如足球机器人、无人机、无人车等.如何保证这些自治机器人尤其是多个机器人在移动过程中的安全成了人们一直很关心的问题.混成通信顺序进程（Hybrid Communicating Sequential Process,HCSP）是一个针对混成系统的形式化建模语言,在通信顺序进程（Communicating Sequential Process,CSP）的基础上引入了微分方程以描述混成系统中的连续行为和控制逻辑,可以方便高效地对大型控制系统尤其是在有通信事件发生时的情形进行形式化建模.本文就是用HCSP建模多机器人的路径控制算法,并用定理证明工具HProver进行形式化验证.结果证明了在满足一定初始条件下,机器人团队在整个运行途中不会发生碰撞.     

混成时空Petri网的CPS实时事件模型

在分析网络物理系统（ CPS）特点的基础上,提出了一种新的CPS体系结构,并对事件进行形式化定义。提出了一种新的CPS物理实体的形式化建模方法。在Petri网的基础上引入时空因素和连续变量,构造了混成时空Petri网（ HSPN）模型,使其不仅能够描述物理实体逻辑和时间层次的行为,而且能够描述物理实体位置变迁所引起的状态变化。将其应用于实时事件CPS模型设计,以医疗控制系统为例,分析建模方法的可行性。     

基于MARTE的面向混成系统的模型形式化转换

混成系统是离散逻辑跳转与实时连续行为交织的复杂状态变迁系统,形式化建模与验证是确保混成系统正确性和可靠性的重要途径。首先介绍一种混成ZIA形式规范;然后,基于建模语言MARTE建立扩展Object-Z的规范,即OZ-MARTE,该规范弥补了MARTE规范在形式化描述方面的不足,同时为了方便描述混成系统中连续动态行为属性,给出对混成系统中连续变量的描述转换规则,增强了MARTE对混成系统的描述能力;最后,给出OZ-MARTE规范到混成ZIA规范的转换方法,因此针对混成ZIA规范的验证技术同样适用于对MARTE模型进行形式化验证。     

一类DEDS状态反馈控制器综合的新方法

对具有无穷状态空间的并发离散事件动态系统提出了一种基于Petri网图示的矩阵代数 综合方法.该方法借助于对Petri网的结构分解可以用于结构无竞争Petri网描述的一类离 散事件动态系统状态反馈控制器的离线综合.     

混成系统研究综述*

混成系统是一类既包含连续动态行为又包含离散动态行为的系统,这类系统在实际应用中显得越来越重要,对这类系统需要探索新的模型和研究方法。从建模、分析与验证三个方面综述了混成系统的研究现状和需要进一步研究的课题。     

点发序列问题的控制策略

在离散事件系统的Petri网模型下,讨论是否存在控制策略使得仅有希望的序列使 能,而又保持事件的并发性的问题.证明了存在这种策略的必要充分条件是给定的目标序 列集是可控的.在目标序列集不可控而所考虑的序列集都是Petri网点发序列集时,提出了 综合给定序列集的极大可控子序列集生成器的方法.     

资源配置混杂Petri网的混杂系统生产过程动态调度

为了增强混杂生产过程应对突发事件的能力,以一种新的混杂Petri网(资源配置混杂Petri网)为研究模型,给出了相应的使能和激发规则.并在资源配置混杂Petri网建立的仿真模型的基础上,融入事件逻辑网和逻辑规划,提出一种适用于混杂系统动态生产调度建模和优化的方法.以典型的混杂生产过程为例,研究混杂系统生产过程建模及优化.研究结果表明,资源配置混杂Petri网模型描述能力强,能够有效描述混杂系统生产过程,所提出的动态调度方案切实有效.     

基于混杂Petri网的交通网络性能分析

本文利用混杂Petri网建模交通系统.通过分析Petri网,得到交通系统的拥塞性质,提出相对拥塞及绝对拥塞的概念,并给出相对拥塞转化为绝对拥塞的条件.结合真实交通数据,形成符合实际交通状况的Petri网实例,得到车辆分布规律,弥补现有智能交通系统仅依赖出租车GPS数据代表车辆分布情况的缺陷.     

化工过程控制混杂系统及其Petri网描述

强调混杂系统的分析，研究了一类化工过程控制系统的混杂系统特性，建立了由过程层、监控层和调度层组成的混杂系统多层混合模型结构。论文分别讨论了各层混杂系统的模型形式，特别对过程控制层混杂系统模型进行了详细的描述。引入Petri网作为描述化工过程控制混杂系统的方法，以化工溶剂回收过程为例，建立了基于混合Petri网的过程控制层的模型。论文的工作为深入研究化工过程控制混杂系统奠定了基础。     

Robot task plan representation by Petri nets: modelling, identification, analysis and execution

In this paper we introduce a framework to represent robot task plans based on Petri nets. Our approach enables modelling a robot task, analysing its qualitative and quantitative properties and using the Petri net representation for actual plan execution. The overall model is obtained from the composition of simple models, leading to a modular approach. Analysis is applied to a closed loop between the robot controller and the environment Petri net models. We focus here on the quantitative properties, captured by stochastic Petri net models. Furthermore, we introduce a method to identify the environment and action layer parameters of the stochastic Petri net models from real data, improving the significance of the model. The framework building blocks and a single-robot task model are detailed. Results of a case study with simulated soccer robots show the ability of the framework to provide a systematic modelling tool, and of determining, through well-known analysis methods for stochastic Petri nets, relevant properties of the task plan applied to a particular environment.     

利用混杂Petri网对基于事件的机器人遥操作系统建模研究

针对采用基于事件思想的移动机器人遥操作系统，首次提出以混杂Petri网作为描 述工具进行建模，模型的离散部分利用传统的Petri网，对应于系统的操作者；连续部分利 用重新定义的便于描述微分代数方程的连续Petri网，对应于位于远端的移动机器人．     

神光III控制系统的故障建模与分析

应用混合随机Petri网对神光III控制系统的故障进行了建模,并应用Visobj Net对建立的故障模型进行了仿真分析。网络化控制系统是一个离散和连续相结合的混合动态系统,具有动态、并发及同步等特征;神光III控制系统就是网络化控制技术在武器装备上的一个典型应用;对于复杂系统的建模和分析,Petri网是一个非常有效的工具。Petri网已经被证明是离散事件或异步系统很好的建模和分析工具,混合随机Petri网是Petri网的一个扩展,具有强大的建模功能。仿真结果表明,所建立的模型是正确的。     

自主式追踪机器人终端行为的Petri网建模*

针对含有资源流动和信息交互的终端行为建模问题,提出了一种混合Petri网行为建模方法。首先,引入活性变迁和惰性变迁两种变迁模式,描述终端行为的耦合、制约、异步关系。其次,建立混合Petri网模型,揭示化学羽流追踪终端各行为之间的交互关系,以Robotics模块为验证与分析工具,仿真机器人终端运动过程,同时获得6个关节角度变化的平稳曲线。最后,在六自由度串联机器人平台加以验证。实验结果表明,该混合Petri网模型客观真实地表达对象内部逻辑关系与交互作用机制,对自主式羽流追踪机器人终端行为建模是有效可行的。     

基于资源配置混杂Petri网的混杂系统生产过程建模

为了增强混杂Ｐｅｔｒｉ网解决资源共享和资源冲突的能力,定义一种新的混杂Ｐｅｔｒｉ网模型———资源配置混杂Ｐｅｔｒｉ网,提出了相应的使能和激发规则．将对连续变迁和离散变迁的控制作用引入混杂Ｐｅｔｒｉ网,同时,增加了资源配置变迁和资源释放变迁,用于有效分配可重复利用的资源．以典型的混杂生产过程为例,研究混杂系统生产过程建模．研究结果表明,所定义的模型描述能力强,模型语义正确合理,能够有效描述和分析混杂系统生产过程．     

Decidability results in First–Order Hybrid Petri Nets

In this paper we tackle the decidabilityof marking reachability for a hybrid formalism based on Petrinets. The model we consider is the untimed version of First–OrderHybrid Petri Nets: it combines a discrete Petri net and a continuousPetri net, the latter being a fluid version of a usual discretePetri net. It is suggested that the decidability results shouldbe pursued exploiting a hierarchy of models as it has been donein the framework of Hybrid Automata. In this paper we definethe class of Single–Rate Hybrid Petri Nets: the continuousdynamics of these nets is such that the vector of the markingderivatives of the continuous places is constant but for a scalarfactor. This class of nets can be seen as the counterpart oftimed automata with skewed clocks. We prove that the reachabilityproblem for this class can be reduced to the reachability problemof an equivalent discrete net and thus it is decidable.