Specification and Verification of Dynamically Reconfigurable Systems Using Dynamic Linear Hybrid Automata

A dynamically reconfigurable system can change its configuration during operation, and studies of such systems are being carried out in many fields. In particular, medical technology and aerospace engineering must ensure system safety because any defect will have serious consequences. Model checking is a method for verifying system safety. In this paper, we propose the Dynamic Linear Hybrid Automaton (DLHA) specification language and show a method to analyze reachability for a system consisting of several DLHAs.

基于统计模型检测的Tc CBTC移动授权建模与分析

基于通信的列车运行控制(communication based train control,CBTC)系统采用车地通信方式使得地面设备极其复杂。随着通信技术的快速发展,以车载为核心的列车运行控制(train-centric communication based train control,TcCBTC)系统采用车车通信方式减少了控制信息的传递环节,将成为城市轨道交通领域的发展方向。移动授权(movementauthority,MA)是决定列车能否以安全间隔运行的直接因素,因此对MA生成过程进行形式化建模与分析,对避免列车碰撞具有重要意义。根据TcCBTC系统架构分析MA生成流程,确定参与功能实现的子系统,并计算出不确定性参数;通过UPPAAL-SMC建立对应的随机混成自动机网络模型;最后采用统计模型检测方法对模型进行定量分析。分析结果表明:置信度为99.95%的情况下,系统在300 ms内成功计算出MA的概率为0.9974124748,为后续TcCBTC系统开发设计提供理论参考。

基于混合自动机的综合能源系统状态转移空间建模

目前对于综合能源系统的建模,更多从系统输入-输出关系、内部状态与输入输出的关系进行描述,其内部状态在不同阶段的转移过程难以清晰表达。在分布式可再生能源占比大幅度提升后,综合能源系统在不同阶段的运行状态及状态转移过程需要可观可控。为此,提出了基于混合自动机的综合能源系统分阶段状态转移空间建模方法,对综合能源系统内部状态的分阶段转移条件及其转移过程进行精准描述,有利于对综合能源系统内部所有能源生产单元和能源消费单元从启动、运行到停止的全过程进行分阶段管理与优化控制。仿真算例表明,所提模型对综合能源系统分阶段的状态转移轨迹实现了全过程观测,有利于实现全过程分阶段的高效管理与优化控制。

ECAS车身高度与整车姿态控制混杂自动机研究

针对电子控制空气悬架(electronically controlled air suspension, ECAS)系统存在明显的混杂动态特征,不易于车身高度和整车姿态精确控制等问题,建立了考虑电磁阀气动特性的ECAS整车非线性机理模型,通过设置车身高度、侧倾角和俯仰角的变化范围设计了描述悬架系统各电磁阀开关切换状态的混杂自动机;利用混合逻辑动态(mixed logical dynamics, MLD)建模方法将所设计的混杂自动机编译为标准MLD模型,从而可直接调整电磁阀的开关状态实现车身高度与整车姿态之间的协调控制;最后对所设计的混杂自动机进行仿真验证。仿真结果表明,该混杂自动机通过对电磁阀开关进行逻辑控制,可以精确地控制车身高度并有效地改善整车姿态,在一定程度上提高了操纵稳定性和乘坐舒适性。

飞走巡线机器人多模式切换混杂控制方法

电力线所处环境恶劣,工况复杂,具柔索特性,对巡线机器人的稳定性和可靠性提出较大挑战,因此以飞走巡线机器人(flying-walking power line inspection robot,FPLIR)为研究对象,提出了一种多模式切换混杂控制方法。在FPLIR巡检工作原理基础上,建立4种控制模式的混杂自动机模型和相互切换的监测器模型;利用Lyapunov函数法和力角稳定性判据(force-angle stability margin,FASM)法分析FPLIR多模式切换和力学特性的稳定性;基于各模式的控制目标,提出了对应的控制策略,尤其结合FPLIR的结构和工况特点,设计变论域模糊控制器,提高FPLIR线上行走的稳定性,设计模型预测控制器,提高FPLIR落线的安全性。最后通过仿真和实验验证了多模式切换混杂控制方法的有效性和可行性,提升了FPLIR在复杂电力线环境下的适应性,为未来机器人智能巡检提供理论参考。

一类混杂系统的推广自动机模型及其仿真

通过分析混杂系统的特点,以混杂系统自动机建模理论为基础,结合一种特殊的并行投影结构(Projection Construct),提出了针对混杂系统的推广自动机模型。该模型着眼于连续状态空间的划分。并行投影结构有效的处理了离散事件动态子系统和连续变量动态子系统之间的接口问题。该方法获得的混杂系统模型由图形的方式表示,简单直观。最后用两个实例介绍了推广自动机模型的建模过程,并借助Matlab环境中的Stateflow工具箱,对模型进行了仿真,结果表明该模型能够很好地解决混杂系统中离散部分和连续部分的同步协调问题。

基于Craig插值的线性混成系统符号化模型检测

最强后件的计算是模型检测算法的核心.本文使用一阶逻辑可满足性模线性算术理论给出线性混成自动机的有界模型检测表示公式,利用一阶逻辑公式不可满足情况下的插值存在性定理,对线性混成自动机的有界模型检测公式进行指定的划分,使用支持线性算术插值计算的可满足性模理论后端证明引擎的线性时间复杂度的消解反证技术获得这两部分公式间的插值公式,按一阶逻辑Craig插值的性质,所得到的插值公式就是模型检测过程中最强后件公式的上近似表示.有效地避免了使用逻辑编码方案实现线性混成自动机模型检测过程中需要双指数时间复杂度的量词消去操作求取最强后件公式,也不需像有界模型检测按步长展开变迁公式进行可满足性判定.最后本文在此最强后件计算的基础上,以有界模型检测技术作为反例确认方法,实现了一种无假反例的混成系统近似可达集计算算法.实验证明该算法与目前已经得到广泛工业应用的有界模型检测算法相比具有更优的性能.

基于混成自动机的CPS行为建模与属性验证

系统实时性、安全性和可靠性等非功能属性是信息物理系统在诸多领域应用的关键因素。论文在分析CPS模型构建与分析验证中面临的挑战的基础上,提出了一种CPS行为建模与属性验证方法。该方法首先基于混成自动机对CPS的行为进行建模,然后将此模型转换为混合程序模型,最后在定理证明器KeYmaera中对HP模型的属性进行形式化验证。文中论述了行为模型描述语言的结构,建立了混成自动机模型与HP模型之间的转换规则,分析了模型转换的一致性。应用实例表明:该方法既能简单直观地描述CPS动态行为,又能对CPS的属性进行严格的形式化验证,且有效避免了形式化验证中的状态空间爆炸问题。

基于混杂系统的风力发电机组建模与控制

针对风力发电机组系统固有的混杂系统典型特征,运用混杂自动机理论和混合逻辑动态理论建立了风力发电机组的混杂模型,设计了基于自动机模型的全程混杂控制系统,并以1台额定功率为300 MW的变速变桨距风力发电机组为例进行了仿真.结果表明:自动机模型可实现风电机组的全程模拟,自动机的混杂控制系统可满足风电机组全程控制的要求,而且基于混合逻辑动态模型的预测控制也实现了功率输出优化,证明了混杂系统理论应用于风力发电研究领域的有效性和实用性.

与线性混杂自动机等价的状态依赖空间模型

混杂系统可以由多种等价系统进行描述,本文研究用状态依赖空间模型对线性混杂自动机进行描述.线性混杂自动机是一类自治的不确定性系统,而状态依赖空间模型是含有输入的确定性系统.在状态依赖空间模型中,通过增加输入变量可以描述线性混杂自动机转换过程中的不确定性,进而将其转换成等价的状态依赖空间模型.本文所提到的等价性是指两个系统产生的轨迹是相同的.

基于混合自动机的PSL模型研究

基于SPICE的计算机仿真方法在混合信号电路验证应用中具有较大的计算开销,讨论基于属性描述的建模方法减小计算开销的问题。通过分析PSL(property specification language)对系统属性的形式化描述方法,并分析混合自动机理论对混合信号系统抽象能力,提出了适合于混合信号电路系统快速验证的PSL模型。结合混合自动机对PSL进行了基于混合自动机语义特点的扩展,使用巴克斯—诺尔范式对其拓展后语法进行规范,提出具有描述混合信号电路行为特性的HAPSL(hybrid automata-based PSL),并针对参考电路的混合信号特性进行了分析,详细说明了HAPSL模型描述在混合信号验证中的实现方法和意义。通过与SPICE仿真器对相同电路进行比较仿真实验,显示HAPSL方法数据在适当规模混合信号电路瞬态分析以及状态分析中具有较高的效率并且具有可接受的精确度。

一类混合系统的建模问题

针对一类具有多个子系统相互作用的混合动态系统,建立了每个子系统的混合输入输出自动机模型,并给出了混合输入输出自动机的运算规则.运用模块化的建模思想,根据子系统之间逻辑和物理上的联系,通过单个模型的输入输出接口,将混合输入输出自动机按照运算规则进行综合,从而建立整个混合系统的混合输入输出自动机模型.通过实例说明了建模方法的运用过程.

混杂系统的扩展时间自动机模型及验证研究

混杂系统复杂度高且涉及领域广,没有通用的方法来解决分析、设计等问题。为解决一类工业控制混杂系统的建模和验证问题,对时间自动机进行了语义扩展,使其含有连续变量以及映射在其上的约束,使用扩展后的时间自动机对此类混杂系统进行建模,采用验证工具UPPAAL进行模型分析模拟,并使用简化的CTL对系统需求规范进行验证。具体实例研究表明,该方法对于分析设计一类混杂系统具有可行性和有效性。

基于混合元胞自动机的铝合金保险杠横梁设计

为提高保险杠横梁的耐撞性并考虑轻量化的要求,提出铝合金横梁结构的设计方法.建立耐撞性有限元仿真模型,基于混合元胞自动机方法进行耐撞性拓扑优化,根据材料分布得到H型梁的结构;采用Kriging近似模型技术,进一步优化拓扑优化后的截面尺寸.结果表明,所提出的结构设计方法可以得到合理的截面形状和尺寸,提高了保险杠横梁耐撞性且实现了轻量化设计.

基于宏观运动波和微观元胞自动机的双车道交通流混合建模

基于运动波理论和线性元胞自动机模型,提出了一种宏观与微观空间表现尺度相结合的双车道交通流混合建模方法.在交通流供需理论框架下,定义了考虑车辆变道行为和元胞自动机空间离散性影响的宏观/微观边界转换条件.该边界条件能够克服在引入车辆变道行为和应用离散化的微观元胞自动机模型时所引起的交通流质量损失问题.应用混合模型模拟双车道堵塞和单车道关闭引起的交通流瓶颈现象.结果表明,交通波在经过模型空间尺度发生变化的边界时能够连续传播,传播速度并未出现降低或者振荡现象,并且交通流质量守恒.混合建模能根据各路段所需表现的空间尺度不同,应用不同空间层次的交通流模型分别模拟,有效提高了大型交通流网络的模拟效能.

基于混杂自动机的大型风力发电机组全程控制

风力发电系统是具有不确定性的复杂非线性系统,机组运行工况变化十分频繁。通过对风力发电机组的系统特性分析,发现风力发电系统呈现出混杂系统的典型特征。因此,基于混杂自动机理论建立了1.5 MW双馈型风电机组的混杂动态模型,并根据风力发电机组控制策略设计了能够在机组运行中实现全程自动化的混杂控制系统。仿真结果表明,基于混杂自动机的动态模型可以实现风电机组的全程模拟,所设计的混杂控制系统能够满足风电机组全程控制要求,证明了混杂系统理论应用于风力发电研究领域的有效性。

基于混合自动机的随机噪声电路动态特性分析

在集成电路非线性随机噪声的分析中应用Petri网技术,需要对原有的Petri网从定义和变迁发射规则方面等进行统计特性与连续特性的拓展研究和补充。并且基于噪声的随机非线性特性分析目的需求,拓展了传统的Petri网,提出了混合随机Petri网(Hybrid Statistical Petri Net,HSPN)模型分析方法。通过分析非线性电路的混合自动机模型,增加Petri网随机参数变迁描述能力,针对电路噪声特点,确定适合HSPN的随机动态特性分析模型。通过实例电路说明验证HSPN的建模方法,并与SPICE仿真软件进行比较,验证了该方法的精度和可行性。

考虑自适应巡航车辆影响的上匝道系统混合交通流模型

在考虑自适应巡航(adaptive cruise control,ACC)车辆的交通流模型的基础上,建立了考虑ACC车辆影响的上匝道系统混合交通流模型,研究ACC车辆引入对上匝道交通系统交通流的影响.为了描述ACC车辆和手动驾驶车辆在交通流运行中的差异,分别构建了基于常车头时距原则的ACC车辆跟驰子模型和手动驾驶车辆MCD元胞自动机子模型;基于上匝道车辆合流驶入主线的需求,建立了换道子模型,引入了表征驾驶员换道心理的参数λ.通过对混合交通流模型进行数值模拟发现,ACC车辆的混入可以有效改善上匝道系统交通流的运行,降低合流等事件对于交通流运行的影响,抑制交通拥堵的时空范围及拥堵强度,提高交通流的平均速度和流量.此外在混合交通流模型中,ACC车辆期望车头时距Hd的减小与换道心理参数λ的增大均可以提高混合交通流运行的速度和流量,而合流区长度lw对混合交通流影响则因上匝道车辆驶入概率的不同而存在差异.

多速率混合系统的模型检查

研究了初始化的多速率混合系统的模型检查问题,即检验初始化的多速率自动机是否满足某个混合区间时序逻辑公式描述的性质.首先定义了一套转换规则把混合区间时序逻辑公式转化为区间时序逻辑公式.接着定义了初始化的多速率自动机状态空间上的等价关系及其对应的域自动机,并且通过构造域自动机对应的标注有限状态自动机,把初始化的多速率混合系统的模型检查问题等价地转换成了可解的区间时序逻辑的模型检查问题.利用区间时序逻辑的模型检查算法加上上述的转换规则,就可以解决初始化的多速率混合系统的模型检查问题.

面向安全攸关系统中小概率事件的统计模型检测

在开放运行环境中,安全攸关系统的不确定性行为有可能导致小概率事件的发生,而此类事件的可靠性指标往往很高,小概率事件一旦发生就会产生灾难性的后果,严重威胁到人们的生命、财产安全.因此,评估、预测小概率事件发生的概率,对于提高系统的可靠性具有重要意义.统计模型检测是一种基于模拟的模型验证技术,结合了系统的快速模拟及统计分析技术,能够有效提高模型检测的效率,适用于验证、评估安全攸关系统的可靠性,但其面临的挑战性问题之一是在可接受的样本数量下,使用统计模型检测技术难以预测、评估小概率事件发生的概率.因此,提出一种改进的统计模型检测框架,设计和开发基于机器学习的统计模型检测器,实现在相对较少的样本数量下预测和评估小概率事件发生的概率.结合轨道交通控制系统中避碰控制案例分析,进一步证明改进后的统计模型检测器能够有效预测和评估安全攸关系统中小概率事件发生的概率.