Abstract
UML-RT is achieving increasing popularity as a modeling language for real-time applications. Unfortunately UML-RT is not formally well defined and it is not well suited for supporting the specification stage: e.g., it does not provide native constructs to represent time and non-determinism. UML+ is an extension of UML that is formally well defined and suitable for expressing the specifications of real-time systems (e.g., the properties of a UML+ model can be formally verified). However, UML+ does not support design and development. This article addresses the translation of UML+ into UML-RT, thus posing the basis for a development framework where UML+ and UML-RT are used together, in order to remove each other’s limitations. Specifications are written using UML+, they are verified by means of formal methods, and are then converted in an equivalent UML-RT model that becomes the starting point for the implementation.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science, n.126 (1994) 183–235
Bertin, V., Closse, E., Poize, M., Pulou, J., Sifakis, J., Venier, P., Weil, D., Yovine, S.: Taxys = Esterel + Kronos. A tool for verifying real-time properties of embedded systems. Conference on Decision and Control, CDC’01. Orlando, IEEE Control Systems Society (2001)
del Bianco, V., Lavazza, L., Mauri, M.: An application of the DESS modeling approach: The Car Speed Regulator, In Proc. SIVOOES 2001, Budapest (2001)
del Bianco, V., Lavazza, L., Mauri, M.: A classification of real-time specifications complexity, In Proc. SIVOOES 2001, Budapest (2001)
del Bianco, V., Lavazza, L., Mauri, M.: An introduction to the DESS approach to the specification of real-time software. CEFRIEL Technical Report RT01002 (2001)
del Bianco, V., Lavazza, L., Mauri, M.: Model Checking UML Specifications of Real Time Software. The Eighth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS02), Greenbelt (2002)
del Bianco, V., Lavazza, L., Mauri, M.: A Formalization of UML Statecharts for Real-Time Software Modeling. The 6th Biennial World Conference On Integrated Design Process Technology (IDPT 2002), “Towards a rigorous UML” session, Pasadena (2002)
Eshuis, R., Wieringa, R.: Requirements-Level Semantics For UML Statecharts. Formal Methods for Open Object-Based Distributed Systems-FMOODS’2000, Stanford (2000)
Ghezzi, C., Mandrioli, D., Morzenti A.: TRIO, a logic language for executable specifications of real-time systems. The Journal of Systems and Software, Vol. 12, n. 2. Elsevier Science (1990)
Heitmeyer C.L., Jeffords R.D., Labaw B.G., Comparing different approaches for Specifying and verifying Real-Time Systems, in Proc. 10th IEEE Workshop on Real-Time Operating Systems and Software, New York (1993) 122–129
Kesten, Y., Pnueli, A.: Timed and Hybrid Statecharts and their Textual Representation. In Formal Techniques in Real-Time and Fault-Tolerant Systems 2nd International Symposium (1992)
Lavazza, L., Quaroni, G., Venturelli, M.: Combining UML and formal notations for modelling real-time systems. In: Gruhn, V. (ed.): Proceedings of ESEC/FSE 2001, Vienna, ACM Press (2001)
Mauri, M.: Estensione di UML per la specifica e la verifica delle proprietà di sistemi Real Time. Politecnico di Milano, Thesis (in Italian), http://www.polimi.it (2001)
OMG: Unified Modeling Language Specification, Version 1.4. http://www.omg.org (2001)
Pnueli A., Shalev, M.: What is in a step: On the semantics of statecharts. In: Ito T., Meyer, A. R. (eds.): Intl. Conf. TACS’ 91: Theoretical Aspects of Computer Software. Lecture Notes in Computer Science, Vol. 526. Springer-Verlag, Berlin Heidelberg New York (1991) 244–264
Rational Software Corporation: Modeling Language Guide, Rational Rose® RealTime, http://www.rational.com (2002)
Reggio, G., Astesiano, E., Choppy C., Hussmann, H.: Analysing UML Active Classes and Associated State Machines-A Lightweight Formal Approach. In Maibaum, T. (ed.): Proc. FASE 2000-Fundamental Approaches to Software Engineering. Lecture Notes in Computer Science, Vol. 1783. Springer-Verlag, Berlin Heidelberg New York (2000)
Selic, B., Gullekson, G., Ward, P. T.: Real-Time Object-Oriented Modeling. Wiley (1994)
Sifakis, J.: Modeling real-time systems-challenges and work directions. EMSOFT01, Tahoe City, October 2001. Lecture Notes in Computer Science, Vol. 2211. Springer-Verlag, Berlin Heidelberg New York (2001)
Yovine, S.: Kronos, A Verification Tool for Real-Time Systems, Kronos User’s Manual Release 2.2. Springer International Journal of Software Tools for Technology Transfer, Vol. 1 October (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Del Bianco, V., Lavazza, L., Mauri, M., Occorso, G. (2003). Towards UML-Based Formal Specifications of Component-Based Real-Time Software. In: Pezzè, M. (eds) Fundamental Approaches to Software Engineering. FASE 2003. Lecture Notes in Computer Science, vol 2621. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36578-8_9
Download citation
DOI: https://doi.org/10.1007/3-540-36578-8_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00899-6
Online ISBN: 978-3-540-36578-5
eBook Packages: Springer Book Archive