Using a formal notation for analysis and verification of a critical system allows its correctness to be ensured and criticality requirements to be satisfied. The UML/OCL notation offers a standard language for high quality Systems modelling. However, the current lack of formal semantics for UMU/OCL explains the existence of few toots supporting analysis and verification of UML models, particularly in the context of railway applications. In this work, we propose an approach providing a formal support of UML based on the B specification language. B provides a formal notation based on the set theory and supported by sophisticated tools allowing specification, refinement, validation and simulation, We aim at providing automated toot support to UML by implementing transformations of class and state-transition diagrams, as well as OCL constraints, into B formal specifications. Our approach is illustrated by developing a railway application: the level crossing System.
UML-based design and formal analysis of railway traffic control systems
UML basierter Entwurf und formale Analyse von Steuerungs- und Regelungssystem für den Zugverkehr
2004
10 Seiten, 10 Bilder, 15 Quellen
Aufsatz (Konferenz)
Englisch
Formal methods for railway operation and control systems
TIBKAT | 2003
|Formal Software Techniques for Railway Systems
British Library Conference Proceedings | 2001
|Towards Domain-Specific Formal Specification Languages for Railway Control Systems
British Library Conference Proceedings | 2001
|Chinese railway traffic control
IuD Bahn | 2002
|