基于随机障碍验证的随机连续系统安全性验证

针对一类同时具有随机初始状态和随机微分方程的随机连续系统的安全性验证问题,提出一种基于随机障碍验证以及初始集选择的计算方法。首先,介绍了随机连续系统及其安全性验证的相关知识及概念;然后,讨论了如何对于服从几种不同分布的初始变量确定初始状态集,并根据选定的初始状态集使用随机障碍验证的方法将安全性验证问题转化为多项式优化问题;最后,运用平方和松弛方法将问题转化为平方和规划问题,并利用SOSTOOLS工具求得安全性概率的下界。理论分析以及实验结果表明,所提方法具有多项式时间的复杂度,能有效地给出随机连续系统在无界时间内的安全性概率的下界。     

一类随机非线性系统的有限时间H∞控制

本文研究一类随机非线性系统的有限时间H_∞控制问题.考虑闭环系统在有限时间间隔内的瞬态性能和抗干扰能力,对伊藤型随机非线性系统进行了研究.利用Lyapunov函数和线性矩阵不等式(LMI)得到了系统满足均方有限时间有界的充分条件,进一步设计了有限时间H_∞控制器,并给出了系统满足均方有限时间有界和相应H_∞性能的充分条件.最后给出了两个例子验证了该方法的有效性和可行性.     

时变时滞连续切换奇异系统的一致有限时间稳定分析

讨论一类含有时变时滞的连续时间切换奇异系统的一致有限时间稳定、有限时间有界和状态反馈镇定问题. 在给定任意的切换规则下, 运用多Lyapunov 函数和平均驻留时间方法设计使得闭环系统一致有限时间稳定和有限时间有界的状态反馈控制器, 同时给出基于线性矩阵不等式表示的控制器存在的充分条件. 最后通过数值算例表明了所提出方法的合理性和有效性.

     

分数阶时变切换系统有限时间异步控制

针对一类时变切换系统,当考虑子系统具有分数阶（Fractional Order）特性时,提出了一种基于模型依赖平均驻留时间方法的有限时间稳定性条件及异步切换控制策略.借助于Caputo分数阶导数引理和切换Lyapunov函数,利用矩阵不等式技术提出了分数阶时变切换系统有限时间稳定的充分条件.将有限时间稳定的结果进一步推广到有限时间有界的情形,利用平均驻留时间思想提出了分数阶时变切换系统有限时间有界的充分条件,基于该条件设计了系统的异步切换控制器.所给出的设计方法将系统异步切换控制问题转化为矩阵不等式组的求解问题.通过数值仿真验证了所提控制方法的有效性.     

一类含多面体不确定性多项式系统鲁棒镇定

针对一类含多面体不确定性的多项式系统,研究其局部稳定鲁棒镇定问题。基于多项式平方和(SOS)技术,将该类非线性控制问题转换为凸的SOS规划问题,并通过引入S-procedure技术,保证了所得结论在局部范围内是有效的。同时,结合参数依赖Lyapunov函数方法,给出了该类系统鲁棒性分析与鲁棒镇定控制问题的充分条件,并将其描述为可由SOS规划技术直接求解的状态依赖线性矩阵不等式约束集。最后,通过数值仿真验证了该方法的有效性。     

线性系统的事件触发输出反馈有限时间有界控制

本文研究了线性系统的事件触发输出反馈有限时间有界控制问题. 与渐近稳定只定性地要求系统在采样间隔 有界不同, 有限时间有界需要估计系统轨迹的上界以保证满足动态系统的定量要求. 本文基于类李雅普诺夫函数给出了 保证闭环系统的有限时间有界性和避免芝诺现象的充分条件. 这些充分条件可以转化为线性矩阵不等式, 便于验证和实 际应用. 此外, 为了节约资源, 提出了一种可变参数的事件触发规则, 提高了设计灵活性. 仿真结果验证了本文的主要结 论.     

基于有限时间的一类时滞非线性切换系统滑模控制

研究一类时滞非线性切换系统的有限时间滑模控制问题.针对所研究的系统模型,构造每个子系统对应的积分滑模面,基于滑模控制理论,设计带有状态时滞的滑模控制器使得每个子系统能在有限时间内到达相应的滑模面上,并对系统中存在的非线性项采用Lipschitz条件进行处理.根据多李亚普诺夫函数、平均驻留时间方法以及分割策略引理,给出滑模趋近段和滑模动态有限时间有界的充分条件,并通过对线性矩阵不等式的求解得到控制器增益.最后,通过一个数值仿真例子验证该设计方法的有效性.     

基于分段多项式李雅普诺夫函数的模糊系统的稳定性分析

本文采用最大型分段多项式李雅普诺夫函数研究了多项式模糊系统的闭环稳定性问题.首先,本文设计了与分段李雅普诺夫函数对应的切换模糊控制器,提出了多项式模糊模型稳定的平方和条件,同时证明了最大型分段多项式李雅普诺夫函数在函数切换点的稳定性.然后,设计了相应的路径跟踪优化算法,对本文非凸的稳定条件进行迭代求解.最后,通过两个算例进行仿真与比较,说明并验证了本文所提出结论的可行有效性.     

一类多项式非线性系统鲁棒H∞控制

针对一类具有多项式向量场的仿射型不确定非线性系统,给出一种基于多项式平方和(sum of squares,SOS)技术的鲁棒H∞状态反馈控制器设计方法.该方法的优点在于控制器的设计避开了直接求解复杂的哈密尔顿-雅可比不等式(Hamilton Jacobi inequality,HJI)和构造Lyapunov函数带来的困难.将鲁棒稳定性分析和控制器设计问题转化为求解以Lyapunov函数为参数的矩阵不等式,该类不等式可利用SOS技术直接求解.此外,在前文基础上研究了基于SOS规划理论与S-procedure技术的局部稳定鲁棒H∞控制器设计方法.最后以非线性质量弹簧阻尼系统作为仿真算例验证该方法的有效性.     

计算机符号积分系统INTG

本文给出了一个新的计算机符号积分系统INTG,可用于求解单变量初等函数的不定积分.该系统已在AI-M16微型机上实现.它可求解使用一种数学手册[1]上的不定积分表所能解决的大部分问题,并具有一定可扩充性.系统使用了符号处理与数值方法相结合的方法求有理函数积分,采用了连分数变换法求整系数多项式的所有实根.系统还可以根据用户要求,显示积分路径的有关信息.     

A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates

This paper presents a methodology for safety verification of continuous and hybrid systems in the worst-case and stochastic settings. In the worst-case setting, a function of state termed barrier certificate is used to certify that all trajectories of the system starting from a given initial set do not enter an unsafe region. No explicit computation of reachable sets is required in the construction of barrier certificates, which makes it possible to handle nonlinearity, uncertainty, and constraints directly within this framework. In the stochastic setting, our method computes an upper bound on the probability that a trajectory of the system reaches the unsafe set, a bound whose validity is proven by the existence of a barrier certificate. For polynomial systems, barrier certificates can be constructed using convex optimization, and hence the method is computationally tractable. Some examples are provided to illustrate the use of the method.     

安全的混成系统神经网络控制器生成与验证

控制器生成是混成系统控制中的重要问题.生成具有安全保证的控制器,关系着混成系统在安全攸关领域的使用.提出了一种为混成系统生成具有安全保证的神经网络控制器的方法.神经网络控制器的安全性由与其同时生成的障碍证书保证.为了生成安全的神经网络控制器,首先确定控制器的网络结构,并基于混成系统构造训练数据集;然后,根据保证控制器安全的障碍证书条件编码神经网络训练时的损失函数.当训练完成后,学习到的神经网络控制器对于训练数据集中的数据是安全的,但对于整个混成系统可能并不安全.为了检验学习到的控制器在整个系统上的安全性,将其安全验证问题转化为一组混合整数规划问题,并使用数值优化器求解,以得到形式化保证的结果.工作实现了安全神经网络控制器生成工具SafeNC,并评估了它在8个基准系统上的性能.实验结果表明:SafeNC可以生成包含6个隐藏层的具有1 804个神经元的安全神经网络控制器;同时,与现有方法相比, SafeNC可为更复杂的系统生成安全的神经网络控制器,更有效且更具扩展性.     

Direct adaptive control for nonlinear matrix second-order dynamical systems with state-dependent uncertainty

A direct adaptive control framework for a class of nonlinear matrix second-order dynamical systems with state-dependent uncertainty is developed. The proposed framework guarantees global asymptotic stability of the closed-loop system states associated with the plant dynamics without requiring any knowledge of the system nonlinearities other than the assumption that they are continuous and lower bounded. Generalizations to the case where the system nonlinearities are unbounded are also considered. In the special case of matrix second-order systems with polynomial nonlinearities with unknown coefficients and unknown order, we provide a universal adaptive controller that guarantees closed-loop stability of the plant states.     

Equilibria, stability and reachability of Leslie systems withnonnegative inputs

Leslie systems, a particular class of positive systems used in population dynamics and control, are defined and analyzed. A simple property relating sign and stability of their equilibria, and some geometric characteristics of their reachability set (in cases of bounded and unbounded inputs) are proved. All the properties do not hold, in general, in other classes of positive systems. It is shown that Leslie systems have strictly positive equilibria if and only if they are asymptotically stable. Their reachability set in the case of unbounded inputs is the positive cone generated by the reachability vectors, while in the case of bounded inputs, it is a polyhedron whose vertices can be easily computed. All of these properties follow from the nonpositiveness of the coefficients of the characteristic polynomial of the system     

Using Forward Reachability Analysis for Verification of Lossy Channel Systems

We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for computing (i) inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop. All these operations are rather simple and can be carried out in polynomial time.With these techniques, one can straightforwardly construct an algorithm which explores the set of reachable states of a protocol, in order to check various safety properties. We also show how one can perform model-checking of LTL properties, using a standard automata-theoretic construction. It should be noted that all these methods are by necessity incomplete, even for the class of protocols with lossy channels.To illustrate the applicability of our methods, we have developed a tool prototype and used the tool for automatic verification of (a parameterized version of) the Bounded Retransmission Protocol.     

On the verification of polynomial system solvers

We discuss the verification of mathematical software solving polynomial systems symbolically by way of triangular decomposition. Standard verification techniques are highly resource consuming and apply only to polynomial systems which are easy to solve. We exhibit a new approach which manipulates constructible sets represented by regular systems. We provide comparative benchmarks of different verification procedures applied to four solvers on a large set of well-known polynomial systems. Our experimental results illustrate the high efficiency of our new approach. In particular, we are able to verify triangular decompositions of polynomial systems which are not easy to solve.     

Highly private blockchain-based management system for digital COVID-19 certificates

As a result of the declaration of the COVID-19 pandemic, several proposals of blockchain-based solutions for digital COVID-19 certificates have been presented. Considering that health data have high privacy requirements, a health data management system must fulfil several strict privacy and security requirements. On the one hand, confidentiality of the medical data must be assured, being the data owner (the patient) the actor that maintain control over the privacy of their certificates. On the other hand, the entities involved in the generation and validation of certificates must be supervised by a regulatory authority. This set of requirements are generally not achieved together in previous proposals. Moreover, it is required that a digital COVID-19 certificate management protocol provides an easy verification process and also strongly avoid the risk of forgery. In this paper we present the design and implementation of a protocol to manage digital COVID-19 certificates where individual users decide how to share their private data in a hierarchical system. In order to achieve this, we put together two different technologies: the use of a proxy re-encryption (PRE) service in conjunction with a blockchain-based protocol. Additionally, our protocol introduces an authority to control and regulate the centers that can generate digital COVID-19 certificates and offers two kinds of validation of certificates for registered and non-registered verification entities. Therefore, the paper achieves all the requirements, that is, data sovereignty, high privacy, forgery avoidance, regulation of entities, security and easy verification.

     

UC-based Approximate Incremental Reachability

In recent years, formal verification technology has received more and more attention, and it plays an important role in ensuring the safety and correctness of systems in safety-critical areas. As a branch of formal verification with a high degree of automation, model checking has a very broad development prospect. This study analyzes and proposes a new model checking technique, which can effectively check transition systems, including bug-finding and safety proof. Different from existing model checking algorithms, the proposed method, Unsatisfiable Core (UC)-based Approximate Incremental Reachability (UAIR), mainly utilizes the UC to solve a series of candidate safety invariants until the final invariant is generated, so as to realize safety proof and bug-finding. In symbolic model checking based on the SAT solver, this study uses the UC obtained by the satisfiability solver to construct the candidate safety invariant, and if the transition system itself is safe, the obtained initial invariant is only an approximation of the safety invariant. Then, while checking the safety, the study incrementally improves the candidate safety invariant until it finds a true invariant that proves the system is safe; if the system is unsafe, the method can finally find a counterexample to prove the system is unsafe. The brand new method exploits UCs for safety model checking and achieves good results. It is known that there is no absolute best method in the field of model checking. Although the proposed method cannot surpass the current mature methods such as IC3 and complement Approximate Reachability (CAR), in terms of the number of solvable benchmarks, the method in this paper can solve three cases that other mature methods are unable to solve. It is believed that the method can be a valuable addition to the model checking toolset.