TRANSPORT. SAFETY AND ECOLOGY. LOGISTICS AND MANAGEMENT
Practical UML subset for railway engineers to support formal modeling
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.