Title :

Component-based modeling and observer-based verification for railway safety-critical applications

Author(s) :

Sango, Marc [Auteur]
Self-adaptation for distributed services and large software systems [SPIRALS]
Laboratoire Électronique Ondes et Signaux pour les Transports [IFSTTAR/COSYS/LEOST]
Duchien, Laurence [Auteur]
Laboratoire d'Informatique Fondamentale de Lille [LIFL]
Self-adaptation for distributed services and large software systems [SPIRALS]
Gransart, Christophe [Auteur]
Laboratoire Électronique Ondes et Signaux pour les Transports [IFSTTAR/COSYS/LEOST]
Self-adaptation for distributed services and large software systems [SPIRALS]

Conference title :

11th International Symposium on Formal Aspects of Component Software

City :

Bertinoro

Country :

Italie

Start date of the conference :

2014-09-10

Publication date :

2014-01-01

Keyword(s) :

Verification
Analyse de systèmes
Système critique
Transport ferroviaire
Sécurité
Logiciel

English keyword(s) :

Software component
Timed automata

HAL domain(s) :

Informatique [cs]/Génie logiciel [cs.SE]

English abstract : [en]

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 ...
Show more >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.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

Comment :

1th International Symposium on Formal Aspects of Component Software , Bertinoro, Italie, 10-/09/2014 - 12/09/2015

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL