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 UML as a front-end for a formal real-time notation. By translating the GRC model into TRIO, we also give formal semantics to some of the UML constructs.

Combining UML and formal notations for modelling real-time systems

LAVAZZA, LUIGI ANTONIO;
2001-01-01

Abstract

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 UML as a front-end for a formal real-time notation. By translating the GRC model into TRIO, we also give formal semantics to some of the UML constructs.
2001
Joint 8th ESEC and 9th ACM SIGSOFT FSE
9781581133905
Joint 8th ESEC and 9th ACM SIGSOFT FSE
Vienna
10-14 September 2001
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11383/17578
 Attenzione

L'Ateneo sottopone a validazione solo i file PDF allegati

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 37
  • ???jsp.display-item.citation.isi??? ND
social impact