Trans Motauto World
Vol. 7 (2022), Issue 2, pg(s) 56-59

TRANSPORT. SAFETY AND ECOLOGY. LOGISTICS AND MANAGEMENT

Practical UML subset for railway engineers to support formal modeling

  • 1 Budapest University of Technology and Economics

Abstract

The acceptance and popularity of formal modeling is increasing in the development of safety-critical railway interlocking systems, because it allows the specification of the system’s functionality using mathematically rigorous rules. The goal of the research described here is to introduce a simple, easy-to-learn, and useful UML (Unified Modeling Language) subset that supports railway engineers in developing the functionality of system elements at the system planning level. The selection of this UML subset is based on our practical experience. We examine the properties and limitations of this subset through a case study using the Yakindu Statechart Tools. The components specified with the proposed UML subset can be easily transformed into timed automata that we studied using the UPPAAL framework. In the paper, we also present the UPPAAL model for the case study. We are currently working on the implementation of a transformation using the UML subset presented in this paper, which makes it possible to generate formal models from Yakindu to UPPAAL in an automated way.

Keywords

References

  1. P. Micouin, Model Based Systems Engineering: Fundamentals and Methods (2014)
  2. R. Bernhard, Modeling with UML (2016)
  3. G. Blokdyk, Sparx Systems Enterprise Architect (2021)
  4. A. Marron, et al., Embedding Scenario-based Modeling in Statecharts, MoDELS (2018)
  5. CENELCE EN 50129, Railway applications – Communication, signalling and processing systems – Safety related electronic systems for signalling (2018)
  6. CENELEC EN 50126, Railway Applications – The Specification and Demonstration of Reliability, Availability, Maintainability and Safety (RAMS) – Part 2: Systems Approach to Safety (2017)
  7. J. Wang, W. Tepfenhart, Formal Methods in Computer Science (2019)
  8. V. Molnár, B. Graics, A. Vörös, I. et al., The Gamma Statechart Composition Framework: Design, Verification and Code Generation for Component-Based Reactive Systems, ICSEC, pp.1-4. (2018)
  9. D. Darvas, Practice-Oriented Formal Methods to Support the Software Development of Industrial Control Systems (2016)
  10. Y. Y. Nazaruddin, T. A. Tamba, K. Pradityo, et al., Safety Verification of a Train Interlocking Timed Automaton Model, IFAC, Vol. 52, Issue 15, pp. 331-335 (2019)
  11. L. Kadakolmath, U. D. Ramu, A Survey on Formal Specification and Verification of Smart Mass Transit Railway Interlocking System, IJSSE, 11(6): 671-682 (2021)
  12. G. Lukács, T. Bartha, Construction of formal models and verifying property specifications through an example of railway interlocking systems, Pollack Periodica, 14(2):39-50 (2019)
  13. C. Bock, et al., Unified Modeling Language 2.5.1 (2017)

Article full text

Download PDF