Reachability-analysis-based verification for safety-critical hybrid systems

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

Method description A detailed description of the method

Hybrid system reachability analysis provides an exhaustive verification alternative to standard simulation-based testing (e.g. Monte-Carlo simulation). Given an appropriate description of the system and a set of inputs, the system evolution over a finite time horizon is computed as a set of reachable states in a specific representation. The representation of reachable states varies among algorithms that solve the problem, and the choices here typically offer various trade-offs between performance and accuracy – note that exact computation of reachable states is an undecidable problem in the general case, therefore what the algorithms typically compute here is an (over)approximation.

Method Strengths A listof the strengths of the method

Automation
Exhaustive coverage
Sound analysis

Method Limitations The limitations of the method

Scalability
False negatives

Method References Bibliography references to papers about the method.

[RAV1] V. A. Tsachouridis, G. Giantamidis, S. Basagiannis, K. Kouramas, “Formal analysis of the Schulz matrix inversion algorithm: A paradigm towards computer aided verification of general matrix flow solvers” in journal Numerical Algebra, Control & Optimization of American Institute of Mathematical Sciences, vol. 10, 2020, doi: 10.3934/naco.2019047.
[RAV2] V. A. Tsachouridis and G. Giantamidis, "Computer-aided verification of matrix Riccati algorithms*", 2019 IEEE 58th Conference on Decision and Control (CDC), Nice, France, 2019, pp. 8073-8078, doi: 10.1109/CDC40024.2019.9030135.
[RAV3] Cimatti A., Griggio A., Mover S., Tonetta S. (2015) HyComp: An SMT-Based Model Checker for Hybrid Systems. In: Baier C., Tinelli C. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2015. Lecture Notes in Computer Science, vol 9035. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46681-0_4.
[RAV4] Chen X., Ábrahám E., Sankaranarayanan S. (2013) Flow*: An Analyzer for Non-linear Hybrid Systems. In: Sharygina N., Veith H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_18.
[RAV5] Frehse G. et al. (2011) SpaceEx: Scalable Verification of Hybrid Systems. In: Gopalakrishnan G., Qadeer S. (eds) Computer Aided Verification. CAV 2011. Lecture Notes in Computer Science, vol 6806. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22110-1_30.

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.