La prochaine réunion du GT VS-CPS Vérification et Synthèse des Systèmes Cyber Physiques et GT MEA aura lieu le
mardi 3 juillet 2018 au CNAM Paris, 10h - 17h.
salle 11B0 (accès 11B, rez-de-chaussée)
salle 11B0 (accès 11B, rez-de-chaussée)
Cnam, 292 rue Saint-Martin, 75003 Paris.
Programme finalisé (8 exposés)
Title. Compositional and quantitative approaches in symbolic control
Author. Antoine Girard
Abstract. Symbolic control aims at designing “correct by construction” controllers for continuous dynamical systems, by using algorithmic discrete synthesis techniques. The key concept in symbolic control is that of symbolic model, which is a finite-state dynamical system, obtained by abstracting continuous trajectories over a finite set of symbols. When the symbolic and the continuous dynamics are formally related by some behavioral relationship (e.g. simulation or bisimulation relations), controllers synthesized for the symbolic model using discrete synthesis techniques can be refined to certified controllers for the original continuous system. In the first part of this talk, I will present some fundamental results on symbolic control from symbolic model computation, to discrete synthesis and controller refinement. Then, I will report some recent progress on scalability and robustness by means of compositional and quantitative synthesis techniques.
Title. Inner and Outer Approximating Flowpipes for Delay Differential Equations
Authors. Sylvie Putot et Eric Goubault
Abstract. Delay differential equations are fundamental for modeling networked control systems where the underlying network induces delay for retrieving values from sensors or delivering orders to actuators. They are notoriously difficult to integrate as these are actually functional equations, the initial state being a function. We propose a scheme to compute inner and outer-approximating flowpipes for such equations with uncertain initial states and parameters. Inner-approximating flowpipes are guaranteed to contain only reachable states, while outer-approximating flowpipes enclose all reachable states. We also introduce a notion of robust inner-approximation, which we believe opens promising perspectives for verification, beyond property falsification. The efficiency of our approach relies on the combination of Taylor models in time, with an abstraction or parameterization in space based on affine forms, or zonotopes. It also relies on an extension of the mean-value theorem, which allows us to deduce inner-approximating flowpipes, from flowpipes outer-approximating the solution of the DDE and its Jacobian with respect to constant but uncertain parameters and initial conditions.
Title. Intervals of a Kleene algebra used to compute inner and outer approximations of invariant sets of a dynamical system
Author. Luc Jaulin.
Abstract. Kleene algebra is a powerful formalism to deal with fixed point methods involving monotonic operators. After defining what is an interval in such an algebra, an interval arithmetic will be presented. Further, we will consider the specific case where the elements of this Kleene algebra are set-valued functions which are automorphism with respect to the intersection. It will be shown how this formalism could help us to build efficient and simple algorithms to compute inner and outer approximations of invariant sets of non-linear continuous-time dynamical systems.
Title: Robust state estimation and fault detection in CPS under noisy environment
Authors: C. Combastel, A. Zolghadri
Abstract: A framework merging the set-membership and the stochastic paradigms is proposed and used in the context of robust state estimation and fault detection of Cyber-Physical Systems (CPS). Set-membership and probabilistic mergers are introduced and particularized to zonotopes and Gaussian signals. They provide a constructive and computationally efficient solution to propagate random uncertainties with incompletely specified probability distributions. Given some confidence level expressed in probabilistic terms (maximal false alarm rate), a detection test is developed and shown to merge the usually mutually exclusive benefits granted by set-membership techniques (robustness to the worst-case within specified bounds, domain computations) and stochastic approaches (taking noise distribution into account, probabilistic evaluation of tests). A distributed implementation on interacting agents will be considered as well as numerical examples illustrating the state estimation capabilities and the improved tradeoff between the sensitivity to faults and the robustness to disturbances/noises.
Title. Vehicle Lateral Dynamics Estimation using Switched Unknown Inputs Interval Observers: Experimental Validation ".
Authors. Sara Ifqir, Naima Ait Oufroukh, Dalil Ichalal and Saïd Mammar.
Abstract. A systematic design methodology for interval estimation of switched uncertain linear systems subject to uncertainties and unknown inputs is presented. The uncertainties under consideration are assumed to be unknown but bounded with a priori known bounds. The proposed observer is used to robustly estimate the vehicle yaw rate and lateral velocity using a vision system measurement. The road curvature is treated as an unknown input and a linear adaptive tire model is considered to take into account the changes of the road adhesion. Sufficient conditions allowing the design of such observer are derived using Multiple Quadratic ISS-Lyapunov function and an LMIs (Linear Matrix Inequalities) formulation is obtained. Performance of the algorithm is evaluated using vehicle real data, results show that the proposed estimation scheme succeeds to appropriately estimate the upper and lower bounds of vehicle lateral dynamics despite of the presence of unknown inputs.
Title. Some new results on mode discernibility and its application to bounded-error state estimation for nonlinear hybrid systems
Authors. Nacim Ramdani, Louise Travé-Massuyès, Carine Jauberthie
Abstract. State estimation is a key engineering problem when addressing control or diagnosis issues for complex dynamical systems. The issue is still challenging when the latter systems must be modelled as hybrid discrete-continuous dynamics, which is true for many complex and safety-critical systems. In this talk, we will report on recent results where we investigate nonlinear hybrid state estimation in a bounded-error framework using reliable and robust methods. We first establish a testable condition for current mode location discernibility. Then we build our hybrid state estimator which relies on a prediction-correction approach. An illustrative example is presented
Title. Formal Verification of Convex Optimization Algorithms For Model Predictive Control
Authors. Paul Rousse
Abstract. The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in safety critical roles. However, this cannot happen without addressing proper attention to the soundness of these algorithms. This work discusses the formal verification of convex optimization algorithms with a particular emphasis on receding-horizon controllers. Additionally, we demonstrate how theoretical proofs of real-time optimization algorithms can be used to describe functional properties at the code level, thereby making it accessible for the formal methods community. In seeking zero-bug software, we use the Credible Auto-coding scheme. We focused our attention on the ellipsoid algorithm solving second-order cone programs (SOCP). In addition to this, we present a floating-point analysis of the algorithm and give a framework to numerically validate the method.
Title. Reachability analysis for mixed discrete/continuous time systems with IQCs and paraboloids.
Authors. Raphael Cohen
Abstract. Finite-time property verification of a dynamical system can be reduced to reachability analysis. For mixed discrete/continuous time systems, number of steps required to evaluate the reachable set is lower-bounded by the frequency of the discrete time part. To avoid this, the discrete time system is replaced by an equivalent continuous time system and the sampler/holder blocks are abstracted by varying delays that verify Integral Quadratic Constrains (IQC). The reachability set of IQC system is over-approximated by time-dependent paraboloids. Parameters of this paraboloid are solution of an initial value problem. An application to a simple mixed discrete/continuous system is presented.