Model Checking of Hybrid Systems with Implicit Semi-Algebraic Abstraction

Improvement of both the applicability and the scalability of model checking techniques for the verification of control software for complex cyber-physical systems.

Method Purpose Short description of the method's purpose and main benefits

Method description A detailed description of the method

Model checking [MHS1, MHS2, MHS3] is a method to verify if a model of the system under verification satisfies its specification. A fundamental step in the verification of control software for complex cyber-physical systems is the analysis of the interaction between the control software with the (controlled) physical plant. Such interaction can be formally represented by hybrid systems, which combine discrete state transitions with continuous dynamics equations.

In this improvement we focus on semi-algebraic abstraction [MHS19], which is an approach to the safety verification problem for polynomial dynamical systems where the state space is partitioned according to the sign of a set of polynomials. Similar to predicate abstraction for discrete systems, the number of abstract states is exponential in the number of polynomials. Hence, semi-algebraic abstraction is expensive to explicitly compute and then analyse (e.g., to prove a safety property or extract invariants). We propose an implicit encoding (as in [MHS20]) of the semi-algebraic abstraction, which avoids the explicit enumeration of the abstract states: the safety verification problem for dynamical systems is reduced to a corresponding problem for infinite-state transition systems, allowing us to reuse existing model-checking tools based on Satisfiability Modulo Theory (SMT). The main challenge that we solve is to express the semi-algebraic abstraction as a first-order logic formula that is linear in the number of predicates, instead of exponential, thus letting the model checker lazily explore the exponential number of abstract states with symbolic techniques. We implemented the approach and validated experimentally its potential to prove safety for polynomial dynamical systems [MHS21].

Method Strengths A listof the strengths of the method

The safety verification problem for dynamical systems is reduced to a corresponding problem for infinite-state transition systems, which enables the use of existing model-checking tools based on Satisfiability Modulo Theory (SMT)
The semi-algebraic abstraction is expressed as a first-order logic formula that is linear in the number of predicates, instead of exponential, which enables the model checker to lazily explore the exponential number of abstract states with symbolic techniques

Method Limitations The limitations of the method

The computation of the reachable states may be too expensive and this approach does not scale to complex models
The semi-algebraic abstraction as a first-order logic formula may be not effective in proving some properties

Method References Bibliography references to papers about the method.

[MHS1] Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press 1999, ISBN 978-0-262-03270-4, https://dl.acm.org/doi/10.5555/332656
[MHS2] Baier, C., Katoen, J.P.: Principles of model checking. MIT Press 2008, ISBN 978-0-262-02649-9, pp. I-XVII, 1-975, https://dl.acm.org/doi/10.5555/1373322
[MHS3] Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer 2018, ISBN 978-3-319-10574-1, https://doi.org/10.1007/978-3-319-10575-8
[MHS19] Sogokon, A., Ghorbal, K., Jackson, P.B., Platzer, A.: A Method for Invariant Generation for Polynomial Continuous Systems. In: Verification, Model Checking, and Abstract Interpretation, VMCAI, pp. 268–288. Springer (2016), https://dx.doi.org/10.1007/978-3-662-49122-5_13
[MHS20] Tonetta, S.: Abstract Model Checking Without Computing the Abstraction. In: Formal Methods, FM, pp. 89–105 (2009), https://doi.org/10.1007/978-3-642-05089-3_7
[MHS21] Mover, S., Cimatti, A., Griggio, A., Irfan, A., Tonetta, S.: Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. Computer Aided Verificartion, CAV (1) 2021: 529-551, https://doi.org/10.1007/978-3-030-81685-8_25

Method Dimensions

Evaluation Environment Type Type of environment where the method is applied. It can be more than one type of environment. (Dimension 1)

Evaluation Type Type of evaluation performed with that method. If a method is hybrid, more than one type can be selected. (Dimension 2)

Type of Component Under Evaluation Type of components that can be evaluated with that method. It can be more than one type. (Dimension 3)

Evaluation Stage The evaluation stage where the method is used. (Dimension 5)

Purpose of the Component Under Evaluation The type of purpose that can be evaluated by a method. It can be more than one type. (Dimension 6)

Type of Requirement Under Evaluation The type of requirements that a method is able to evaluate. It can be more than one type. (Dimension 7)

Evaluation Performance Indicator The type of evaluation criteria or KPI that a method is able to improve. It can be more than one type. (Dimension 8)

Relations

Related Methods A method could be related to other methods.

Tools A method can use zero or more tools.

Part Method A method (when it is a combination: Combination of method artefact that is a specialization of a V&V Method) could be composed of a set of V&V Methods.

Test Case or Verification and Validation activity Test Case or V&V activity performed in a Use Case. We will link to the method to the test cases where the method is used.

Standards A method can be linked with standards.

Context

Workflow

Contents

There are currently no items in this folder.