Combining UML and formal notations for modelling real-time systems

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 appraoch is applied to the Generalised Railroad Crossing (GRC) problem, one of the best known benchmarks porposed 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.

REFERENCES

• 1: Douglass B. P. Real-Time UML, Addison Wesley, 1998.
• 2: C. Ghezzi , D. Mandrioli , A. Morzenti, TRIO: A logic language for executable specifications of real-time systems, Journal of Systems and Software, v.12 n.2, p.107-123, May 1990 [doi>10.1016/0164-1212(90)90074-V]
• 3: C. L. Heitmeyer , R. D. Jeffords , B. G. Labaw, Comparing different approaches for specifying and verifying real-time systems, Proceedings of the tenth IEEE workshop on Real-time operating systems and software, p.122-129, March 1993, New York, New York, United States
• 4: Mandrioli D., Morzenti A., Pezze M., San Pietro P., Silva S., A Petri Net and Logic Approach to the Specification and Verification of Real-Time Systems, Trends in Software n.5, Heitmeyer C. and Mandrioli D. Eds., Wiley, 1996
• 5: OMG, Unified Modeling Language Specification Version 1.3, First Edition, March 2000.
• 6: Bran Selic , Garth Gullekson , Paul T. Ward, Real-time object-oriented modeling, John Wiley & Sons, Inc., New York, NY, 1994
• 7: Dino Mandrioli , Sandro Morasca , Angelo Morzenti, Generating test cases for real-time systems from logic specifications, ACM Transactions on Computer Systems (TOCS), v.13 n.4, p.365-398, Nov. 1995 [doi>10.1145/210223.210226]
• 8: Yovine S., Kronos: A Verification Tool for Real-Time Systems. In Springer International Journal of Software Tools for Technology Transfer, 1,(October 1997).
• 9: Quaroni G. and Venturelli M., Utilizzo integrato di UML e TRIO per la specifica di sistemi Real Time, Politecnico di Milano, February 2001, Thesis (in Italian).
• 10: OMG, XML Metadata Interchange (XMI) Specification, Version 1.0, June2000, available at http://www.omg.org/technology/documents/formal/xml_meta data_interchange.htm
• 11: Alberto Coen-Porisini , Matteo Pradella , Pierluigi San Pietro, A Finite-Domain Semantics for Testing Temporal Logic Specifications, Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.41-54, September 14-18, 1998
• 12: Miguel Felder , Angelo Morzenti, Validating real-time systems by history-checking TRIO specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.4, p.308-339, Oct. 1994 [doi>10.1145/201024.201034]
• 13: http://www.rational.com/
• 14: http://argouml.tigris.org/

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.7 COMPUTERS IN OTHER SYSTEMS
      Subjects: Real time

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: UML

General Terms:
Design, Languages, Verification

Keywords:
UML, formal methods, real-time software