SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 03:00 - 03:20 at SPLASH-IV - Papers Chair(s): Liqian Chen, Khalil Ghorbal

Cyber-physical systems (CPSs), as cruise control systems, involve life-critical or mission critical functions that must be validated. Formal verification techniques can bring high assurance level but have to be extended to embrace all the components of CPSs. Physical part models of CPSs are usually defined from ordinary differential equations (ODEs) and reachability methods can be used to compute safe over-approximation of the solution set of ODEs. However, additional constraints, as obstacle avoidance have also to be considered to validate CPSs. To meet this need, we propose in this paper a framework, based on abstract domains, for solving constraint satisfaction problems where the objects manipulated are described by ODEs. We use a form of disjunctive completion for which we provide a split operator and an efficient constraint filtering mechanism that takes advantage of the continuity aspect of ODEs. We illustrate the benefits of our method on a real-world application of trajectory validation of a swarm of drones, for which the main property we aim to prove is the absence of collisions between drone trajectories. Our work has been concretized in the form of a cooperation between the DynIbex library, used for the abstraction of ODEs, and the AbSolute constraint solver, used for the constraint resolution. Experiments show promising results.

Tue 17 Nov

Displayed time zone: Central Time (US & Canada) change

03:00 - 04:20
PapersNSAD at SPLASH-IV
Chair(s): Liqian Chen National University of Defense Technology, China, Khalil Ghorbal Inria, France
03:00
20m
Paper
Abstract Domains for Constraint Programming with Differential Equations
NSAD
03:20
20m
Paper
Numeric Domains Meet Algebraic Data Types
NSAD
Santiago Bautista Univ Rennes, ENS Rennes, Inria, IRISA, Thomas P. Jensen INRIA Rennes, BenoƮt Montagu Inria
03:40
20m
Paper
Proving array properties using data abstraction
NSAD
Julien Braine , Laure Gonnord University of Lyon & LIP, France
04:00
20m
Paper
Rigorous Linear Programming Techniques for Numerical Abstract Domains
NSAD
Tengbin Wang , Liqian Chen National University of Defense Technology, China, Ji Wang