Improved Invariant Generation for Industrial Software Model Checking of Time Properties - CentraleSupélec Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

Improved Invariant Generation for Industrial Software Model Checking of Time Properties

Résumé

Modern automotive embedded software is mostly designed using model-based design tools such as Simulink or SCADE, and source code is generated automatically from the models. Formal proof using symbolic model checking has been integrated in these tools and can provide a higher assurance by proving safety-critical properties. Our experience shows that proving properties involving time is rather challenging when they involve long durations and timers. These properties are generally not inductive and even advanced techniques such as PDR/IC3 are unable to handle them on production models in reasonable time. In this paper, we first present our industrial use case and comment on the results obtained with the existing model checkers. Then we present our invariant generator and methodology for selecting invariants according to physical dimensions. They enable the proof of properties with long-running timers. Finally, we discuss their implementation and benchmarks.
Fichier principal
Vignette du fichier
Improved Invariant Generation for Industrial Software Model Checking of Time Properties.pdf (805.33 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02322576 , version 1 (05-10-2020)

Identifiants

Citer

Vassil Todorov, Safouan Taha, Frédéric Boulanger, Armando Hernandez. Improved Invariant Generation for Industrial Software Model Checking of Time Properties. 2019 IEEE 19th International Conference on Software Quality, Reliability and Security (QRS), Jul 2019, Sofia, Bulgaria. pp.334-341, ⟨10.1109/QRS.2019.00050⟩. ⟨hal-02322576⟩
161 Consultations
208 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More