Model Checking of Hybrid Systems

Application 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. Many languages to specify the model exist and range from finite-state to infinite-state machines, from discrete-time to timed or hybrid systems, from non-deterministic automata to stochastic models, from synchronous to asynchronous communicating programs.

A fundamental step in the verification and validation of control software for complex cyber-physical systems is the analysis of the interaction with the controlled physical plant. Such interaction can be formally represented by hybrid systems, which combine discrete state transitions with continuous dynamics equations. There exist several model checking techniques and tools specialized for hybrid systems. These tools are mainly focused on the verification of invariants and most of them compute an over-approximation of the set of the reachable states. HYTECH [MHS4] is a model checker for linear hybrid automata, which represents the continuous part of the reachable states using polyhedra. PHAVER [MHS5] and SPACEEX [MHS6] model affine continuous dynamics with inputs. They check invariant properties computing an approximation of the set of the reachable states using different techniques (polyhedra and support functions). Other model checkers, HSOLVER [MHS7], D/DT [MHS8], ARIADNE [MHS9], FLOW* [MHS10] verify invariants of non-linear hybrid systems. KEYMAERA [MHS11] is a theorem prover for hybrid systems. It can handle non-linear hybrid systems, with symbolic parameters and an unbounded number of components.
Other tools and techniques are based on SMT-based model checking. HyCOMP [MHS12] is a symbolic model checker for hybrid systems built on top of the NUXMV model checker [MHS13], and implements various verification techniques based on SMT (e.g., BMC, K-induction, IC3). HYCOMP can verify invariant and LTL properties [MHS14], and scenario specifications [MHS15]; it can also perform synthesis of parameters ensuring the satisfaction of a given (invariant) property [MHS16].

HybridSAL [MHS17] is very similar to HYCOMP. The tool encodes linear hybrid systems as infinite-state transition systems, which can be verified using the SAL [MHS18] model checker. HybridSAL also implements other abstraction techniques (e.g., see [MHS19]), but only for invariant properties.

In the fragment of timed automata, the reference tool is UPPAAL [MHS20]. It supports model checking of a subset of TCTL (Timed Computation Tree Logic) properties. The reachability is explicit in the discrete states of the automata.

Method Strengths A listof the strengths of the method

Automatic - making model checkers relatively easy to use
Can check for specific properties without verifying the full system
Exhaustively explores the state space
Well-established verification tools and techniques with industrial applications

Method Limitations The limitations of the method

The computation of the reachable states or of the abstraction may be too expensive and the techniques do not scale to complex models
Abstraction techniques may be too coarse and 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
[MHS4] Henzinger, T.A., Ho, P., Wong-Toi, H.: HYTECH: A Model Checker for Hybrid Systems. STTT 1(1-2), 110–122 (1997), https://doi.org/10.1007/s100090050008
[MHS5] Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. STTT 10(3),263–279 (2008), https://doi.org/10.1007/s10009-007-0062-x
[MHS6] Frehse, G., Guernic, C.L., Donz ́e, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable Verification of Hybrid Systems. In: CAV. pp. 379–395 (2011), https://doi.org/10.1007/978-3-642-22110-1_30
[MHS7] Ratschan, S., She, Z.: Safety Verification of Hybrid Systems by Constraint Propagation-Based Abstraction Refinement. ACM Trans. Embedded Comput. Syst. 6(1) (2007), https://doi.org/10.1007/978-3-540-31954-2_37
[MHS8] Asarin, E., Dang, T., Maler, O.: The d/dt Tool for Verification of Hybrid Systems. In: CAV. pp. 365–370 (2002), https://dl.acm.org/doi/10.5555/647771.757171
[MHS9] Benvenuti, L., Bresolin, D., Collins, P., Ferrari, A., Geretti, L., Villa, T.: Assume -Guarantee Verification of Nonlinear Hybrid Systems with ARIADNE. International Journal of Robust and Nonlinear Control 24(4), 699–724 (2014), https://onlinelibrary.wiley.com/doi/10.1002/rnc.2914
[MHS10] Chen, X., ́Abrah ́am, E., Sankaranarayanan, S.: Flow*: An Analyzer for Non-linear Hybrid Systems. In: Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. pp. 258–263 (2013), https://doi.org/10.1007/978-3-642-39799-8_18
[MHS11] Platzer, A., Quesel, J.: KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description). In: IJCAR. pp. 171–178 (2008), https://doi.org/10.1007/978-3-540-71070-7_15
[MHS12] Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: An SMT-Based Model Checker for Hybrid Systems. TACAS 2015: 52-67, https://doi.org/10.1007/978-3-662-46681-0_4
[MHS13] Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S.,Roveri, M., Tonetta, S.: The nuXmv Symbolic Model Checker. In: CAV. pp. 334–342 (2014), https://doi.org/10.1007/978-3-319-08867-9_22
[MHS14] Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Verifying LTL Properties of Hybrid Systems with K-Liveness. In: CAV. pp. 424–440 (2014), https://doi.org/10.1007/978-3-319-08867-9_28
[MHS15] Cimatti, A., Mover, S., Tonetta, S.: SMT-based scenario verification for hybrid systems. Formal Methods in System Design 42(1), 46–66 (2013), https://doi.org/10.1007/s10703-012-0158-0
[MHS16] Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Parameter synthesis with ic3. In: FMCAD. pp. 165–168 (2013), https://doi.org/10.1109/FMCAD.2013.6679406
[MHS17] Tiwari, A.: HybridSAL Relational Abstracter. In: CAV. pp. 725–731 (2012), https://doi.org/10.1007/978-3-642-31424-7_56
[MHS18] de Moura, L.M., Owre, S., Rueß, H., Rushby, J.M., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: CAV. pp. 496–500 (2004), https://doi.org/10.1007/978-3-540-27813-9_45
[MHS19] Sogokon, A., Ghorbal, K., Jackson, P.B., Platzer, A.: A Method for Invariant Generation for Polynomial Continuous Systems. In: 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: FM, pp. 89–105 (2009), https://doi.org/10.1007/978-3-642-05089-3_7

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.