2015 | OriginalPaper | Buchkapitel
Formal Verification of Industrial Critical Software
verfasst von : Marielle Petit-Doche, Nicolas Breton, Roméo Courbis, Yoann Fonteneau, Matthias Güdemann
Erschienen in: Formal Methods for Industrial Critical Systems
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In this paper, the challenges for using formal verification based on automatic tools, like model-checkers, in the industrial development process of safety critical systems is discussed. This usage must be integrated into an appropriate process and must allow for independent result-checking.
Our approach is illustrated with a case study from the
openETCS
ITEA2 research project using the Systerel Smart Solver S3, a modern SAT-based model-checker for equivalence checking and safety properties analysis of
SCADE
, C or Ada programs.