UML-based Railway Interlocking (UML-based RI) is proposed as a methodology in designing and developing Railway Interlocking Systems (RIS). It consists of infrastructure objects and UML is used to model the system behavior. This design is validated and demonstrated by using simulation with Rhapsody. The applied method to verify the systems automatically and formally is model checking. The model and checking conditions are put into the model checker NuSMV. This conventional way in applying model checking leads to the state space explosion problem. Multi-object checking is a method that can be applied to solve this problem and this approach in verifying a UML-based RI is investigated.
Simulation and verification of UML-based Railway Interlocking Systems
Simulation und Verifikation von auf UML basierten Bahn-Signaltechnik-Systemen
2007
10 Seiten, 8 Bilder, 11 Quellen
Conference paper
English
Verification of Railway Interlocking - Compositional Approach with OCRA
British Library Conference Proceedings | 2016
|Modelling Railway Interlocking Systems
British Library Conference Proceedings | 2001
|