Component-based modeling and observer-based verification for railway safety-critical applicationsReport as inadecuate

Component-based modeling and observer-based verification for railway safety-critical applications - Download this document for free, or read online. Document in PDF available to download.

1 SPIRALS - Self-adaptation for distributed services and large software systems Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 2 IFSTTAR-COSYS-LEOST - Laboratoire Électronique Ondes et Signaux pour les Transports 3 LIFL - Laboratoire d-Informatique Fondamentale de Lille

Abstract : One of the challenges that engineers face, during the development process of safety-critical systems, is the verification of safety application models before implementation. Formalization is important in order to verify that the design meets the specified safety requirements. In this paper, we formally describe the set of transformation rules, which are defined for the automatic transformation of safety application source models to timed automata target models. The source models are based on our domain-specific component model, named SARA, dedicated to SAfety-critical RAilway control applications. The target models are then used for the observer-based verification of safety requirements. This method provides an intuitive way of expressing system properties without requiring a significant knowledge of higher order logic and theorem proving, as required in most of existing approaches. An experimentation over a chosen benchmark at rail-road crossing protection application is shown to highlight the proposed approach.

en fr

Keywords : Software component Timed automata

Mots-clés : Verification Analyse de systèmes Système critique Transport ferroviaire Sécurité Logiciel

Author: Marc Sango - Laurence Duchien - Christophe Gransart -



Related documents