FEANICSES 2019 Workshop

Buses and subway are operated by Tisséo (https://www.tisseo.fr/). There is a mobile app to help design a trip.

Two main options to come to ISAE-Supaero:

• metro B (subway), towards Ramonville, stop at Faculté de Pharmacie. Then
  • either bus 78 towards Saint Orens, stop at ENAC. Walk on avenue Édouard Belin on your left. Entrance is at about 300m.
  • or bus 27 and stop at ISAE-SUPAERO

From the airport, use the Tram or the bus to reach Toulouse center.

Polyhedron representation is widely used in the field of static analysis by abstract interpretation, to express the invariants of program. These invariants are used to verify the safety of programs.

The use of the polyhedron invariants makes the analysis very expressive but also very time consuming.

The idea is to find a good trade off between the expressiveness and the time execution. For that, we propose in this article an optimisation method to over-approximate the polyhedron invariant by minimizing the loss of precision.

This talk presents a framework based on robust control theory to aid in the certification process of unmanned aircraft system (UAS) flight controllers. Uncertainties are characterized and quantified based on mathematical models and flight test data obtained in-house for a small, commercial, off-the-shelf platform with a custom autopilot. These uncertainties are incorporated via a linear fractional transformation to model the uncertain UAS. Utilizing integral quadratic constraint (IQC) theory to assess the uncertain UAS worst-case performance, it is demonstrated that this framework can determine system sensitivities to uncertainties, compare the robustness of controllers, tune controllers, and indicate when controllers are not sufficiently robust. To ensure repeatability, this framework is used to tune, compare, and analyze a suite of controllers, including path-following, trajectory-tracking, H-infinity, H2, and PID controllers. By employing a non-deterministic simulation environment and conducting numerous flight tests, it is shown that the uncertain UAS framework reliably predicts loss of control, compares the robustness of different controllers, and provides tuned controllers which are sufficiently robust. Furthermore, robust performance guarantees from IQC analysis can be used to provide worst-case bounds on the UAS state at each point in time, providing an inexpensive and robust mathematical tool to aid in the certification of UAS flight controllers.

We consider the problem of approximating the reachable set of a continuous or discrete-time polynomial system from a semialgebraic set of initial conditions under general semialgebraic set constraints. Assuming inclusion in a given simple set like a box or an ellipsoid, we provide a method to compute certified outer approximations of the reachable set.

The proposed method consists of building a hierarchy of relaxations for an infinite-dimensional moment problem. Under certain assumptions, the optimal value of this problem is the volume of the reachable set and the optimum solution is the restriction of the Lebesgue measure on this set. Then, one can outer approximate the reachable set as closely as desired with a hierarchy of super level sets of increasing degree polynomials. For each fixed degree, finding the coefficients of the polynomial boils down to computing the optimal solution of a convex semidefinite program. When the degree of the polynomial approximation tends to infinity, we provide strong convergence guarantees of the super level sets to the reachable set. We also present some application examples together with numerical results.

This talk will present a method to compute an approximation of the maximum positively invariant (MPI) set, assuming only the knowledge of finitely many samples (x, x^+) produced by an unknown and possibly nonlinear dynamical system x^+ = f(x). The method is based on a novel characterization of the MPI set via the solution to an infinite-dimensional linear programming problem in the space of continuous functions with the minimizer attained and of known Lipschitz regularity. This facilitates the convergence analysis of the resulting approximation scheme, providing rates of converge as well as bounds on the number of samples required to obtain an outer approximation of the MPI set with high probability.

We present a framework for introducing high-level require- ment specifications in the automated analysis of dataflow models. By integrating the FRET requirements elicitation tool with the CoCoSim analyzer, our framework enables the analysis of hierarchical Simulink models against requirements written in a restricted English language. More precisely, we support: automatic extraction of Simulink model information and association of high-level requirements with target model signals and components; translation of temporal logic formulas into synchronous dataflow CoCoSpec specifications as well as Simulink monitors; and interpretation of counterexamples produced by the analysis both at the requirement and model level. The features provided by our framework are generic and can be used to integrate other requirements elicitation and Simulink/Lustre analysis tools. We report on the lessons learned from the application of our approach to the Lockheed Martin Cyber-Physical, aerospace-inspired challenge problems. For the analysis, we used the Kind2, Zustre, and Simulink Design Verifier (SLDV) tools.

The talk will be divided into two separate yet related parts. The first will revisit a result by Liu, Zhan and Zhao [EMSOFT 2011] about the decidability of the positive invariance of semi-algebraic sets. We will give a different intuitive proof in terms of inward/outward flow. The second part of the talk focuses on using symbolic methods for proving the non-existence of invariant algebraic sets. The method will be in particular show-cased for the van der Pol oscillator.

For a given dynamical system, we compute a reachable tube overapproximation by combining different analyzing framework in a fixed point algorithm. Our method have many common points with co-simulation approaches with the difference that all the computations are set-based and that the primary objective is not computational performance but rather the specialization of the different solvers.

At each steps, the system is abstracted to fit a family of models. We use a solver that is specialized for this family of models. We then compute a valid overapproximation of the reachable tube. This algorithm is repeated until a fixed point is reached. We apply this method to compute the reachable set of an hybrid dynamical system with continuous and discrete time subparts.

In this talk, we address the problem of optimizing the types of data (formats) used in floating-point programs. As the highest precision of the types of data can degrade significantly the program's performance, we are implementing a new automated tuning tool based on a static program analysis approach.

The proposed approach aims to combine a forward and backward static analysis. The forward analysis propagates safely the errors on the inputs and on the results of the intermediary operations in order to determine the accuracy of the results. After, depending on the results of the forward analysis and on assertions indicating the accuracy of the user, the backward analysis computes the minimal precision needed for the inputs and intermediary results in order to satisfy these assertions. Moreover, we express our analysis as a set of constraints made of propositional logic formulas and relations between affine expressions over integers. Then, these constraints can be easily checked by an SMT solver. Thus, the results of the previous analysis may help to reduce the types of data that represent the values stored in the floating-point variables of programs.

Over the last few years, Neural Networks have become increasingly popular and have now started penetrating safety critical domains and embedded systems such as autonomous driving cars, rockets, robots, etc. in which they are often taking important decisions.

These Neuronal Networks become larger and larger while embedded systems still have limited resources (Memory, CPU, Computing power, etc.) As a consequence, using and running large Neural Networks on embedded systems with limited resources introduce several new challenges. Recent work has focused on safety and robustness (AI2,DeepPoly,Sherlock). A different approach is shown here which concerns Fixed Point and Integer Arithmetic.

Neuronal Networks are developed on computers with a powerful computing unit that consumes a lot of energy using the floating point arithmetic. Exporting an Neural Network using Fixed-Point and Integer Arithmetic can disturb and change the answer and the behavior of the Neural Network. To use these large Neural Networks on embedded systems, a new approach is needed to adapt Neuronal Network computations with small CPU. It consists of using fixed point and integer arithmetic because it is quick and easy to manipulate for a CPU with less energy.

Since scientific computations keeps being more and more complex, guaranteeing the final result of a program relying on computer arithmetic remains a very hard task. However, during program execution, roundoff error can be accumulated and lead to faulty execution. In this presentation, we propose a new dependent type system for checking numerical stability in finite precision using prametrized gauge functions for dataflow languages like Lustre. Its dependent type contains ufp (unit in the first place) value which is used to estimate maximum value of roundoff error. The type check fails if there can be a computation result whose roundoff error becomes larger when solving constraints about the ufp values.

Some mathematical proofs involve intensive computations, for instance: the four-color theorem, Hales' theorem on sphere packing (formerly known as the Kepler conjecture) or interval arithmetic. For numerical computations, floating-point arithmetic enjoys widespread usage thanks to its efficiency, despite the introduction of rounding errors.

Formal guaranties can be obtained on floating-point algorithms based on the IEEE~754 standard, which precisely specifies floating-point arithmetic and its rounding modes, and a proof assistant such as Coq, that enjoys efficient computation capabilities. Coq offers machine integers, however floating-point arithmetic still needed to be emulated using these integers.

A modified version of Coq is presented that enables using the machine floating-point operators. The main obstacles to such an implementation and its soundness are discussed. Benchmarks show potential performance gains from two to three orders of magnitude.

The formal verification and validation of real-world, industrial critical hybrid flight controllers remains a very challenging task. An increasingly popular and quite successful alternative to formal verification is the use of optimization and reinforcement learning techniques to maximize some real-valued reward function encoding the robustness margin to the falsification of a property. In this paper we present an evaluation of a simple Monte-Carlo Tree Search property falsification algorithm, applied to select properties of a longitudinal hybrid flight control law: a threshold overshoot property, two frequential properties, and a discrete event-based property.

In this talk we propose an algorithm for generating explicit solutions of multiparametric mixed-integer convex programs to within a given suboptimality tolerance. The algorithm is applicable to a very general class of optimization problems, but is most useful for hybrid model predictive control, where on-line implementation is hampered by the worst-case exponential complexity of mixed-integer solvers. The output is a simplicial partition which defines a static map from the current state to a suboptimal solution. In this talk, we shall introduce a novel non-zero optimal cost overlap metric which is necessary and sufficient for convergence. The overlap size is also linked to partition complexity. The algorithm is massively parallelizable and our implementation, which is publicly available (https://github.com/dmalyuta/explicit_hybrid_mpc), has been run on a cluster of several hundred processors. Not only does our solution have a deterministic runtime, simulations show that our approach is faster than on-line optimization by up to three orders of magnitude.

In this presentation, we are interested in deciding whether a given set is an invariant for a piecewise-affine dynamical system. The proposed method is based on matrices norm defined from a piecewise quadratic Lyapunov function. The method is the natural extension of the one presented last year at the Feanicses meeting.

The study of computer-controlled systems presents a number of challenges both from the perspective of computer-theory and automatic control. One of this challenge concerns the analysis of the dynamical performances of such a system. This talk is aimed at approaching this problem from an automatic-control perspective through the theory of sampled-data systems.

In particular, a widespread framework for control design of Linear Time Invariant systems is recalled to define what one may actually refer to when speaking about "dynamical performances". To analyse how these performances may carry out in the real implemented computer-controlled system, established results and tools from sampled-data systems theory are introduced.

In this talk, we aim at presenting a framework for the analysis of continuous and sampled-data models analysis. This proposed framework and underlying techniques are rooted on the interpolatory tools largely used in the model approximation framework. We will try to show that such a method family may be a practical and affordable toolset for attacking such complex interconnected models analysis.

At 7:30pm, l'Oncle Pom in Toulouse, not far from ENSEEIHT, St Aubin church and le Canal du Midi.

At 7:30pm, la Cendrée, next to Esquirol place, the heart of Toulouse.

At 8pm, le Saint Sauvage, next to St Sernin basilica, Toulouse downtown.