混合系统的形式验证技术及其在化工过程控制中的应用

针对PLC等逻辑控制器控制连续对象的可靠性问题。给出了混合系统的形式验证的方法,即用混合矩形自动机建模,通过其商迁移的可达性分析,证明了控制程序的正确性,应用实例表明该方法是可行和有效的。     

一类非线性系统最大可控不变集求解

针对非线性系统线性化在状态约束下最优鲁棒控制求解问题,提出了一种基于混合系统的非线性系统最大鲁棒控制不变集的方法.对于一类非线性系统通过平衡点线性化的方法转化为多模态的混合系统,并进行了混合逻辑动态模型(MLD)的建模,在不变集基本理论的基础上,通过多参数规划的混合整数规划(MIQP)的方法迭代求解最大可控不变集,并求得不变集内的最优控制器,解决系统的状态约束问题.通过一个非线性系统的实例进行建模、仿真,证明了本方法的可行性.     

基于进化粒子滤波器的混合系统故障诊断

在混合系统中，需要同时估计系统的混合状态和系统参数．针对存在这类故障的混合系统的混合状态和参数估计问题提出一种解决方案，对混合系统使用混合自动机建模，并使用粒子滤波算法对其混合状态进行估计，对可能发生变化(故障)的参数使用进化粒子滤波算法进行估计，从而实现了混合系统的故障诊断．将这二者结合起来构成混合系统故障诊断的应用框架，实现了混合系统的混合状态和系统参数的在线估计．仿真结果表明所提出的应用框架和方法是可行的．     

混合系统在matlab环境下的建模和仿真

混合系统是集连续动态系统和离散事件为一体的复杂动态系统,是近年来控制理论研究领域的热门课题.由于混合系统既含连续变量义含离散事件,给处理这类系统带来了复杂性.一般混合系统建立模方法有:混合自动机,混合petri,时段演算及其扩展等模型.在概述混合系统概念与特点的基础上,介绍了混合系统研究中的建模与仿真问题.结合超市冰柜系统用混合自动机建模,并用MATLAB中的SIMULINK和STATEFLOW进行仿真.仿真结果表明效果很好,为系统分析和设计提供了有力的工具.     

基于混合系统模型的非线性系统最大可控不变集求解

针对非线性系统线性化在状态约束下最优鲁棒控制求解问题,提出了一种基于混合系统的分段仿射系统(PWA)建模,通过多次优化迭代的方法求解系统的最大鲁棒控制不变集的方法,并求得不变集内的最优控制器,解决系统的状态约束问题.通过一个非线性系统实例进行建模、仿真,证明了本方法的可行性.     

基于混合系统状态估计的故障诊断

如果将故障的发生视为一个离散事件,则存在故障可能的系统可以看作随机混合系 统,那么故障诊断问题就可转化为混合系统的离散状态估计问题.文中试图从这个角度研究 在非高斯噪声环境下非线性系统的故障诊断问题.在发生故障后的系统模型是已知的假定条 件下,使用随机混合自动机对系统建模,并利用基于粒子滤波的混合估计算法估计出混合状 态,从而完成故障诊断.仿真结果表明,所提的方法是可行的,可以处理某类故障诊断.     

混合系统的建模设计与仿真综述

混合系统是一类既包含连续动态行为又包含离散动态行为的系统,这类系统在实际应用中显得越来越重要,对这类系统需要探索新的模型和研究方法。该文在概述混合系统概念、特点以及发展近况的基础上,主要综述了近年来混合系统研究中的一些重要问题,指出现有各种方法的优缺点,并指出了今后的研究方向。该文首先介绍了混合系统研究中多种常见的建模方法,如混合自动机、Petri网和时段演算,然后重点讨论了混合系统一些重要性质,主要集中在对系统稳定性、可达性、可观性的分析方法上,以及混合系统的多种设计方法,并且对这些方法进行了初步评价,最后介绍了混合系统研究中一些常用的仿真工具。     

混合系统的稳定性分析

研究了混合系统的稳定性问题.首先,对于混合系统给出了一种一般的模型,该模型能 够描述混合状态的跳变现象.然后,定义了一种辅助函数作为系统能量的一种度量.基于该模型 和辅助函数,得到了混合系统稳定性判定的一些新结果.这些结果给出了在离散状态改变时,在 由于连续状态的跳变而引起的系统能量增加的情况下,混合系统仍保持稳定的充分条件.最后， 给出了一种能量函数的寻找方案,并利用一个仿真实例验证了该方案的有效性.     

混合投影时序逻辑与混合系统的形式化验证

为了描述混合系统的性质和行为，10多年来，各种时序逻辑，如Hybrid Temporal Logic等相继出现。这些时序逻辑适用于刻画混合系统的性质和规范，但不适宜表示描述系统的实现模型。本文定义了一个混合投影时序逻辑（Hybrid Projection Temporal Logic，简称HPTL），既能刻画混合系统的性质，又能表示混合系统的实现。这样，混合系统的验证就可以很方便地在统一的数学模型框架下进行。同时，给出了HPTL的基本的逻辑等价式系统和一个用HPTL进行混合系统验证的实例。     

混合系统剖析,描述与建模

混合系统是一种离散和连续构件交织的系统。通常以微分方程为连续模型，以离散事件系统或自动机为离散模型。通过分析混合系统的微观结构，文中提出了面向系统设计的描述语言ＤＤＬ。它能直观、精确刻画混合现象，方便设计决策描述，而且通过控制器符号与系统指称约束的延迟，为系统设计带来很大的灵活性。由ＤＤＬ描述的混合系统，经内部通信隐藏和系统单步协调积，可转换为混合变迁系统。     

Symbolic Algorithmic Analysis of Rectangular Hybrid Systems

This paper investigates symbolic algorithmic analysis of rectangular hybrid systems.To deal with the symbolic reachability problem,a restricted constraint system called hybrid zone is formalized for the representation and manipulation of rectangular automata state-spaces.Hybrid zones are proved to be closed over symbolic reachability operations of rectangular hybrid systems.They are also applied to model-checking procedures for verifying some important classes of timed computation tree logic formulas.To ...     

基于多面体包含的非线性混成系统可达性分析

针对一类非线性混成系统的可达性问题,提出了一种基于多面体包含的分析方法。首先介绍了混成系统及其可达性,讨论了如何应用多面体包含对多项式混成系统进行线性近似,并采用量词消去和非线性优化方法来构造相应的线性混成系统,然后运用验证工具SpaceEx求得原非线性混成系统的过近似可达集,并应用于验证系统的安全性。     

BACH:线性混成系统有界可达性模型检验工具

混成自动机的模型检验问题非常困难,即使是其中相对简单的一个子类--线性混成自动机,它的可达性问题仍然是不可判定的.现有的相关工具大都使用多面体计算来判定线性混成自动机状态空间的可达集,复杂度高、效率低,无法解决实际应用规模的问题.描述了一个面向线性混成系统有界可达性模型检验工具--BACH(bounded reacha...     

LDPChecker一个实时和混成系统模型检验工具

混成系统是一类复杂系统,线性混成系统作为其重要子类,在形式方法中,人们通常使用线性混成自动机来对它建模．虽然线性混成自动机的模型检验问题总的来说还是不可判定的,但对于其中的正环闭合自动机．其对于线性时段性质的满足性能够通过线性规划方法加以检验．为了实现自动检验正环闭合自动机对线性时段性质的满足性,设计并实现了工具LDPChecker．工具LDPChecker能够识别正环闭合自动机并对其进行相应的检验,其主要特色在于它能够对实时和混成系统检验包含可达性在内的许多实时性质,并且能够自动给出诊断信息．     

非线性DEDS的标准结构

非线性DEDS是指由极大极小函数描述的系统, 常见于计算机科学、控制论、运筹学等领域, 考虑非自治非线性DEDS的结构问题, 通过引入白色图和凝白色图, 得到了系统能达和能观的两个充要条件以及系统的标准结构, 同时还给出了它们的矩阵表示.     

基于迁移系统分析的线性混成系统安全验证

混成自动机行为中既包含离散行为又包含连续行为,非常复杂。其安全性验证问题难以解决,即使是线性混成自动机,它的可达性问题也被证明是不可判定的。现有工具大都使用多面体计算来计算线性混成自动机的可达状态空间集,复杂度高,可处理问题规模非常有限。为了避免这类问题,实现了一种新的工具。该工具将线性混成自动机表达为等价的迁移系统,并利用迁移系统上不变式生成相关工作对混成自动机进行验证。实验数据表明,方法有效可行,工具具有良好的性能。     

Assume–guarantee verification of nonlinear hybrid systems with Ariadne

In many applicative fields, there is the need to model and design complex systems having a mixed discrete and continuous behavior that cannot be characterized faithfully using either discrete or continuous models only. Such systems consist of a discrete control part that operates in a continuous environment and are named hybrid systems because of their mixed nature. Unfortunately, most of the verification problems for hybrid systems, like reachability analysis, turn out to be undecidable. Because of this, many approximation techniques and tools to estimate the reachable set have been proposed in the literature. However, most of the tools are unable to handle nonlinear dynamics and constraints and have restrictive licenses. To overcome these limitations, we recently proposed an open‐source framework for hybrid system verification, called Ariadne , which exploits approximation techniques based on the theory of computable analysis for implementing formal verification algorithms. In this paper, we will show how the approximation capabilities of Ariadne can be used to verify complex hybrid systems, adopting an assume–guarantee reasoning approach. Copyright © 2012 John Wiley & Sons, Ltd.     

On the analysis of nonlinear nilpotent switched systems using the Hall–Sussmann system

We consider an open problem on the stability of nonlinear nilpotent switched systems posed by Daniel Liberzon. Partial solutions to this problem were obtained as corollaries of global nice reachability results for nilpotent control systems. The global structure is crucial in establishing stability. We show that a nice reachability analysis may be reduced to the reachability analysis of a specific canonical system, the nilpotent Hall–Sussmann system. Furthermore, local nice reachability properties for this specific system imply global nice reachability for general nilpotent systems. We derive several new results revealing the elegant Lie-algebraic structure of the nilpotent Hall–Sussmann system.     

Analysis of Hybrid Systems Based on Hybrid Net Condition/Event System Model

In thispaper, hybrid net condition /event systems are introducedas a model for hybrid systems. The model consists of a discretetimed Petri net and a continuous Petri net which interact eachother through condition and event signals. By introducing timeddiscrete places in the model, timing constraints in hybrid systemscan be easily described. For a class of hybrid systems that canbe described as linear hybrid net condition /eventsystems whose continuous part is a constant continuous Petrinet, two methods are developed for their state reachability analysis.One is the predicate-transformation method, which is an extensionof a state reachability analysis method for linear hybrid automata.The other is the path-based method, which enumerates all possiblefiring seqenences of discrete transitions and verifies if a givenset of states can be reached from another set by firing a sequenceof discrete transitions. The verification is performed by solvinga constraint satisfaction problem. A technique that adds additionalconstraints to the problem when a discrete state is revisitedalong the sequence is developed and used to prevent the methodfrom infinite enumeration. These methods provide a basis foralgorithmic analysis of this class of hybrid systems.