Simulation and Verification of UML-based Railway Interlocking Designs - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2006

Simulation and Verification of UML-based Railway Interlocking Designs

Résumé

The development of safety critical systems such as railway interlocking systems demands the application of formal methods in order to verify the operativeness and the safety of the system. In this contribution we outline our approach of developing a UML-based Railway Interlocking System. The feasibility of the basic functionality is demonstrated by simulation. In order to verify the system under development, we apply model checking for the verification of specifications that belong to a single object. We tackle the state space explosion problem in those cases in which a number of objects is related to a checking condition by the application of multi-object checking. As multi-object checking is only limited by the state space of the largest object (a point in our case), multi-object checking will be applied successfully to verify the system (e.g ensure the absence of conflicting routes). First results of a case study promise the near future of fully automatic verification of complete station layouts and all desired routes.
Fichier principal
Vignette du fichier
AVOCSRIS.pdf (392.19 Ko) Télécharger le fichier

Dates et versions

inria-00091664 , version 1 (06-09-2006)

Identifiants

  • HAL Id : inria-00091664 , version 1

Citer

Yuen Man Hon, Maik Kollmann. Simulation and Verification of UML-based Railway Interlocking Designs. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.168-172. ⟨inria-00091664⟩

Collections

AVOCS06
183 Consultations
698 Téléchargements

Partager

Gmail Facebook X LinkedIn More