scholarly journals Tool Presentation: Isabelle/HOL for Reachability Analysis of Continuous Systems

10.29007/b3wr ◽  
2018 ◽  
Author(s):  
Fabian Immler
Keyword(s):  
Distinctive Feature ◽  
Reachability Analysis ◽  
Theorem Prover ◽  
Continuous Systems ◽  
Affine Arithmetic ◽  
Discretization Errors ◽  
Runge Kutta

We present a tool for reachability analysis of continuous systems based onaffine arithmetic and Runge-Kutta methods. The distinctive feature of our toolis its verification in the interactive theorem prover Isabelle/HOL: thealgorithm is guaranteed to compute safe overapproximations, taking into accountall round-off and discretization errors.

scholarly journals Optimizing Safe Control of a Networked Platoon of Trucks Using Reachability

10.29007/kxk7 ◽  
2018 ◽  
Author(s):  
Ibtissem Ben Makhlouf ◽  
Stefan Kowalewski
Keyword(s):  
Design Process ◽  
Support Function ◽  
Control Design ◽  
Complex Interaction ◽  
Reachability Analysis ◽  
Networked Systems ◽  
Continuous Systems ◽  
Safe Control

The problem of conceiving a controller for networked systems is a challenging taskbecause of the complex interaction of its different components with each other and also with the environment around them. The design process becomes more difficult if large-scaled systems are involved. We propose reachability analysis of continuous systems to guarantee control requirements which because of the complexity of the problem could not be taken into account during the control design. As example we suggest a large-scalable platoon of trucks. We use our own support function implementation to assess the performances of the obtained controlledplatoon and then decide about the best performing controller.

scholarly journals ARCH-COMP17 Category Report: Continuous Systems with Nonlinear Dynamics

10.29007/v6g4 ◽  
2018 ◽  
Author(s):  
Xin Chen ◽  
Matthias Althoff ◽  
Fabian Immler
Keyword(s):  
Nonlinear Dynamics ◽  
Formal Verification ◽  
Hybrid Systems ◽  
Reachability Analysis ◽  
Current Status ◽  
Continuous Systems ◽  
Friendly Competition

We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. This year, three tools CORA, Flow* and Isabelle/HOL (in alphabetic order) participated. They are applied to solve the reachability analysis problems on three benchmarks which have 2, 7 and 12 variables respectively. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools. Besides, the computational settings presented here provide a guide to use the tools although they might not be optimal.

scholarly journals Pegasus: sound continuous invariant generation

2021 ◽  
Author(s):  
Andrew Sogokon ◽  
Stefan Mitsch ◽  
Yong Kiam Tan ◽  
Katherine Cordwell ◽  
André Platzer
Keyword(s):  
Hybrid Systems ◽  
Experimental Evaluation ◽  
Discrete Systems ◽  
Automatic Generation ◽  
Theorem Prover ◽  
Continuous Systems ◽  
Formal Proofs ◽  
Deductive Verification ◽  
Invariant Generation ◽  
Discrete Invariants

AbstractContinuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.

scholarly journals Deductive Stability Proofs for Ordinary Differential Equations

2021 ◽  
pp. 181-199
Author(s):  
Yong Kiam Tan ◽  
André Platzer
Keyword(s):  
Differential Equations ◽  
Ordinary Differential Equations ◽  
Real World ◽  
Formal Analysis ◽  
Dynamic Logic ◽  
Logical Structure ◽  
Theorem Prover ◽  
Continuous Systems ◽  
Stability Properties ◽  
Controlled Systems

AbstractStability is required for real world controlled systems as it ensures that those systems can tolerate small, real world perturbations around their desired operating states. This paper shows how stability for continuous systems modeled by ordinary differential equations (ODEs) can be formally verified in differential dynamic logic (). The key insight is to specify ODE stability by suitably nesting the dynamic modalities of with first-order logic quantifiers. Elucidating the logical structure of stability properties in this way has three key benefits: i) it provides a flexible means of formally specifying various stability properties of interest, ii) it yields rigorous proofs of those stability properties from ’s axioms with ’s ODE safety and liveness proof principles, and iii) it enables formal analysis of the relationships between various stability properties which, in turn, inform proofs of those properties. These benefits are put into practice through an implementation of stability proofs for several examples in KeYmaera X, a hybrid systems theorem prover based on .

Sign in / Sign up

Export Citation Format

Share Document