Invited Talks

Challenges on the Application of Formal Methods for Validation and Verification in Aerospace Systems Engineering
Leonardo Mangeruca, Orlando Ferrante, Alberto Ferrari
(United Technologies Research Center, Rome, Italy)
Needs in formal methods for the validation of naval systems
Adrien Derock, Agathe Jouven, Laurent Raffaeli (Naval Group, France)
Compositional Taylor Model Based Validated Integration
Kristjan Liiva, Paul Jackson, Grant Passmore and Christoph Wintersteiger
Automatic Generation and Formal Verification of an Interior Point Algorithm
Pierre-Loïc Garoche (ONERA Toulouse, France)
Towards Enumerative Invariant Synthesis in SMT Solvers
Andrew Reynolds (University of Iowa, USA)
Verified Probabilistic Reachability in Parametric Hybrid Systems: Theory and Tool Implementation
Paolo Zuliani (Newcastle University, UK)
Parallel reachability analysis of hybrid systems in XSpeed
Rajarshi Ray (NIT Meghalaya, India)
The Policy Iterations Algorithm is Actually a Newton Method
Assalé Adjé (University of Perpignan, France)

Program Details

9.00 - 10.30 : Needs and Challenges in the Aerospace and Naval Domains

9.00 - 9.45

Challenges on the Application of Formal Methods for Validation and Verification in Aerospace Systems Engineering
Leonardo Mangeruca, Orlando Ferrante, Alberto Ferrari
(United Technologies Research Center, Rome, Italy)
Abstract. The complexity of modern aircraft development is rising constantly pushed by the growth of the transportation market, the continuous technology improvements, the rising of new technologies, the development of more challenging regulations and the ever increasing competition. The high cost investments involved with the development of an aircraft and its constituent systems leads airframers and system suppliers to take critical design decisions early, with a potentially high risk on the development and operational costs of the aircraft. On the other hand, the increasing complexity makes the costs and risks connected with the verification and testing of aircraft systems and their integration constantly rising.
These considerations are pushing the aerospace industry towards growing deployment of model-based methods to anticipate design problems closer in time to when the design decisions are taken, to reduce the risk of turn-backs and migrate towards a virtual testing driven development process to gradually achieve right-the-first-time test rig campaigns and safety-of-flight.
In this evolving landscape, promising model-based technologies beyond simulation are emerging to support this view, including property falsification, automatic test generation and coverage and formal verification technologies. Nonetheless, there still remain compelling challenges to overcome to render these technologies widely applicable across the aerospace industry. In this paper, we present such challenges and position them in context of the development process of aerospace systems and relevant aerospace engineering standards. (Back to Top)

9.45 - 10.30

Needs in formal methods for the validation of naval systems
Adrien Derock, Agathe Jouven, Laurent Raffaeli (Naval Group, France)
Abstract. Naval systems are becoming more and more complex as they are increasingly integrated with a significant increase in software parts. The complexity also comes from many modes in systems ranging from complete automation to secondary modes requiring the intervention of human operators. Validation naval systems must take into account all these aspects which are no longer manageable without the assistance of computer tools. This presentation will present examples of naval systems as well as properties to verify, for which real failures have been observed and for which the use of formal methods is necessary. A focus on performance properties and software validation will be realized during this presentation. The purpose of this presentation is to stimulate discussions between the industrial needs of formal validation in naval systems and the current academic solutions that could address these issues. (Back to Top)

10.30 – 11.00 : Coffee Break



11.00 – 12.30 : Methods (Session 1)

11.00 – 11.30

Compositional Taylor Model Based Validated Integration
Kristjan Liiva, Paul Jackson, Grant Passmore and Christoph Wintersteiger
Abstract. We present a compositional validated integration method based on Taylor models. Our method combines solutions for lower dimensional subsystems into solutions for a higher dimensional composite system, rather than attempting to solve the higher dimensional system directly. We have implemented the method in an extension of the Flow* tool. Our preliminary results are promising, suggesting significant gains for some biological systems with nontrivial compositional structure. (Back to Top)

11.30 - 12.00

Automatic Generation and Formal Verification of an Interior Point Algorithm
Pierre-Loïc Garoche (ONERA Toulouse, France)
Abstract.With the increasing power of computers, real-time algorithms tends to become more complex and therefore require better guarantees of safety. Among algorithms sustaining autonomous embedded systems, model predictive control (MPC) is now used to compute online trajectories, for example in the SpaceX rocket landing. The core components of these algorithms, such as the convex optimization function, will then have to be certified at some point. This paper focuses specifically on that problem and presents a method to formally prove a primal linear programming implementation. We explain how to write and annotate the code with Hoare triples in a way that eases their automatic proof. The proof process itself is performed with the WP-plugin of Frama-C and only relies on SMT solvers. Combined with a framework producing all together both the embedded code and its annotations, this work would permit to certify advanced autonomous functions relying on online optimization. (Back to Top)

12.00 - 12.30

Towards Enumerative Invariant Synthesis in SMT Solvers
Andrew Reynolds (University of Iowa, USA)
Abstract. In the past several years, syntax-guided synthesis (SyGuS) solvers have made significant progress as efficient backend reasoners in several applications. One approach for syntax-guided synthesis, as implemented in the SMT solver CVC4, has shown that SMT solvers can act as efficient stand-alone tools for synthesis. This talk focuses on a new enumerative approach for invariant synthesis in the SMT solver CVC4. We describe a divide-and-conquer approach that makes use of an evolving set of refinement lemmas that constrain concrete points of the invariant-to-synthesize. We show its applicability to synthesis in multiple SMT domains, including for synthesizing invariants that involve non-linear arithmetic. (Back to Top)

12.30 – 14.00 : Lunch



14.00 – 15.30 : Methods (Session 2)

14.00 – 14.30

Verified Probabilistic Reachability in Parametric Hybrid Systems: Theory and Tool Implementation
Paolo Zuliani (School of Computing, Newcastle University, UK)
Abstract. Parametric Hybrid Systems (PHS) model systems whose behaviour is mixed continuous/discrete and can depend on parameters which can be stochastic (i.e., random) or nondeterministic (no distribution is known). Such models are useful for describing, e.g., cyber-physical systems and biological systems. In this talk, we present our recent work on bounded probabilistic reachability for PHS. Specifically, we aim at computing the probability that the system reaches a given region of its state space in a given number of discrete steps and finite time. We present an algorithm that is guaranteed to compute an arbitrarily precise approximation of the probability for a reasonably large class of PHS (so-called robust systems). The algorithm has been implemented in the ProbReach tool, which is available at https://github.com/dreal/probreach. (Back to Top)

14.30 - 15.00

Parallel reachability analysis of hybrid systems in XSpeed
Rajarshi Ray (NIT Meghalaya, India)
Abstract. Reachability analysis techniques are at the core of the current state-of-the-art technology for verifying safety properties of cyber-physical systems (CPS). In this talk, I will present a suite of parallel state-space exploration algorithms in the tool XSpeed that, leveraging multi-core CPUs, enable to improve the performance of reachability analysis of linear continuous and hybrid automaton models of CPS. A performance evaluation on several benchmarks comparing their key performance indicators will be shown. This enables to identify the ideal algorithm and the parameters to choose that would maximize the performances for a given benchmark. (Back to Top)

15.00 - 15.30

The Policy Iterations Algorithm is Actually a Newton Method
Assalé Adjé (University of Perpignan, France)
Abstract. The talk highlights the closed link between the policy iterations algorithm and the Newton method. The main different between them comes from the very special differential operator used for policy iterations algorithm. We show that the policy iterations algorithm is sub-optimal in the sense that it does not fully exploit the information provided by this special differential. Finally, we propose correlations between the hypothesis that ensure the convergence of the algorithms.(Back to Top)

15.30 – 16.00 : Coffee Brak

16.00 – 17.00 : Discussion and Concluding Remarks

19.00 - 21.30 : Workshops dinner at Keble College Back to Top

Sponsors