Combining UML and formal notations for modelling real-time systems

This article explores a dual approach to real-time software development. Models are written in UML, as this is expected to be relatively easy and economic. Then models are automatically translated into a formal notation that supports the verification of properties such as safety, utility, liveness, etc. In this way, developers can exploit the advantages of formal notations while skipping the complex and expensive formal modelling phase. The proposed approach is applied to the Generalised Railroad Crossing (GRC) problem, one of the best known benchmarks proposed in the literature. A UML model of the GRC is built, and then translated into TRIO (a first order temporal logic). The resulting specification properties are tested by a history checking tool which exploits the formality of TRIO. The work described here highlights the shortcomings of UML as a real-time modelling language, proposes enhancements and workarounds to overcome UML limitations, and demonstrates the viability of using U...

• Type: Conference
• Year: 2001
• Where: SIGSOFT
• Authors: Luigi Lavazza, Gabriele Quaroni, Matteo Venturelli
• Keywords: Expensive Formal Modelling, Formal Real-time Notation, SIGSOFT 2001, Software Engineering, UML Limitations