Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Software and Systems Modeling
Published in: Software and Systems Modeling 1/2016

20-02-2014 | Regular Paper

An executable formal semantics for UML-RT

Authors: Ernesto Posse, Juergen Dingel

Published in: Software and Systems Modeling | Issue 1/2016

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We propose a formal semantics for UML-RT, a UML profile for real-time and embedded systems. The formal semantics is given by mapping UML-RT models into a language called kiltera, a real-time extension of the \(\pi \)-calculus. Previous attempts to formalize the semantics of UML-RT have fallen short by considering only a very small subset of the language and providing fundamentally incomplete semantics based on incorrect assumptions, such as a one-to-one correspondence between “capsules” and threads. Our semantics is novel in several ways: (1) it deals with both state machine diagrams and capsule diagrams; (2) it deals with aspects of UML-RT that have not been formalized before, such as thread allocation, service provision points, and service access points; (3) it supports an action language; and (4) the translation has been implemented in the form of a transformation from UML-RT models created with IBM’s RSA-RTE tool, into kiltera code. To our knowledge, this is the most comprehensive formal semantics for UML-RT to date.
previous article A profile and tool for modelling safety information with design information in SysML
next article Evaluating the appropriateness of the BPMN 2.0 standard for modeling service choreographies: using an extended quality framework

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Appendix
Available only for authorised users
Footnotes
1
In the \(\pi \)-calculus literature, this is known as scope extrusion as the lexical scope of the private name is effectively extended beyond its original scope.
 
2
Note that since we assume unique names for all connection points, the source and target of a transition are well defined.
 
3
If the state has no parent, i.e., it is the top-most state on the state machine, the role of the parent will be taken by a special process called \( Sink \), described in Definition 8.
 
4
If the state has no parent, i.e., it is the top-most state on the state machine, the role of the parent will be taken by a special process called \( Sink \), described in Definition 8.
 
5
Note that the processes \(Q_{i}\) and \(Q'_{i}\) are very similar but differ in the parameters passed to the target state: \(Q'_{i}\) deals with incoming transitions, so the primed channels \( inp' ,\, acc' ,\, rej' ,\, exit' ,\, exack' ,\, sh' \), and \( kill' \) are passed to the target sub-state so that it may interact with state \(n_{k}\)’s \( Handler \). On the other hand, \(Q_{i}\) deals with both incoming and sibling transitions, and therefore, in the sibling transition case, it passes on the non-primed channels \( inp ,\, acc ,\, rej ,\, exit ,\, exack ,\, sh \), and \( kill \) so that the target state becomes the currently active sub-state of its parent and thus can communicate with the parent’s \( Handler \).
 
6
In kiltera, channels are bidirectional, allowing both input and output on the same port. Nevertheless, we represent each UML-RT port (respectively, connector) by a pair of kiltera ports (respectively, channels) to differentiate between input and output on a port.
 
Literature
1.
Benghazi Akhlaki, K., Capel Tuñón, M.I., Holgado Terriza, J.A., Mendoza Morales, L.E.: A methodological approach to the formal specification of real-time systems by transformation of UML-RT design models. Sci. Comput. Program. 65, 41–56 (2007)
2.
3.
Bertolino, A., De Angelis, G., Bartolini, C., Lipari, G.: A UML Profile and a Methodology for Real-Time Systems Design. Technical Report, Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo” (2005)
4.
de Melo Bezerra, J., Hirata, C.M.: A Semantics for UML-RT Using \(\pi \)-Calculus. In: Proceedings of International Workshop on Rapid System Prototyping (RSP’07) (2007)
5.
de Melo Bezerra, J., Hirata, C.M.: A polyadic pi-calculus approach for the formal specification of UML-RT. Adv. Softw. Eng. 2009, (2009). doi:10.​1155/​2009/​656810
6.
Boudol, G.: Asynchrony and the \(\pi \)-Calculus (Note). Technical Report 1702, INRIA-Sophia Antipolis (1992)
7.
Capel, M.I., Mendoza, L.E., Akhlaki, K.B., Holgado, J.A.: A semantic formalization of UML-RT models with CSP+T processes applicable to real-time systems verification. In: Proceedings of Jornadas de Ingeniería del Software y Bases de Datos (JISBD’06), pp. 283–292 (2006)
8.
9.
Damm, W., Josko, B., Pnueli, A., Votintseva, A.: Understanding UML: a formal semantics of concurrency and communication in real-time UML. In: Proceedings of FMCO’02. LNCS, pp. 71–98. Springer, Berlin (2002)
10.
Dingel, J., Paen, E., Posse, E., Rahman, R., Zurowska, K.: Definition and implementation of a semantic mapping for UML-RT using a timed pi-calculus. In: Proceedings of the Second International Workshop on Behaviour Modelling: Foundation and Applications, BM-FA ’10, pp. 1:1–1:8. ACM, New York, NY (2010)
11.
Douglass, B.P.: Real-time UML. Formal Techniques in Real-Time and Fault-Tolerant Systems, Volume 2469 of LNCS, pp. 53–70. Springer, Berlin (2002)
12.
Engels, G., Heckel, R., Küster, J.M., Groenewegen, L.: Consistency-preserving model evolution through transformations. In: Proceedings of the Fifth International Conference on the Unified Modeling Language—The Language and its Applications, pp. 212–227. Springer, Berlin (2002)
13.
Eshuis, R., Wieringa, R.: A Formal Semantics for UML Activity Diagrams—Formalising Workflow Models. Technical Report. University of Twente (2001)
14.
Fecher, H., Kyas, M., De Roever, W.-P., De Boer, F.S.: Compositional operational semantics of a UML-Kernel-model language. Electron. Notes Theor. Comput. Sci. 156, 79–96 (2006)CrossRef
15.
Ferreira, P., Sampaio, A., Mota, A.: Viewing CSP specifications with UML-RT diagrams. Electron. Notes Theor. Comput. Sci. 195(0), 57–74 (2008). Proceedings of the Brazilian Symposium on Formal Methods (SBMF 2006)
16.
Fischer, C., Olderog, E.-R., Wehrheim, H.: A CSP view on UML-RT structure diagrams. In: Proceedings Fundamental Approaches to Software Engineering (FASE’01), Volume 2029 of LNCS, pp. 91–108. Springer, Berlin (2001)
17.
Garlan, D., Monroe, R.T., Wile, D.: Acme: architectural description of component-based systems. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems, Chapter 3, pp. 47–67. Cambridge University Press, New York, NY (2000)
18.
Grosu, R., Broy, M., Selic, B., Stefanescu, G.: Behavioral Specifications of Businesses and Systems, Chapter 6: What is Behind UML-RT?, pp. 73–88. Kluwer, Dordrecht (1999)
19.
20.
Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: Proceedings of ECOOP ’91, Volume 512 of LNCS, pp. 133–147. Springer, Berlin (1991)
21.
IBM: General Description Language. IBM, 9 March (2005)
22.
23.
24.
IEEE Computer Society: IEEE Standard \(\text{ Verilog }^{\textregistered }\) Hardware Description Language, IEEE Standard \(1364^{{\rm TM}}\)-2001, 28 September (2001)
25.
IEEE Computer Society: IEEE Standard VHDL Language Reference Manual, IEEE Standard \(1076^{{\rm TM}}\)-2008, 26 January (2009)
26.
IEEE Computer Society: IEEE Standard for the SystemC Language, IEEE Standard \(1666^{\rm TM}\)-2011, January (2012)
27.
IEEE Computer Society: IEEE Standard for SystemVerilog—Unified Hardware Design, Specification, and Verification Language, IEEE Standard \(1800^{\rm TM}\)-2012, 21 February (2013)
28.
International Telecommunications Union: Specification and description language (SDL). ITU-T Recommendation Z.100., November (1999)
29.
30.
Lano, K., Clark, D.: UML 2 Semantics and Applications. Chapter Ch. 8—Axiomatic Semantics of State Machines, pp. 179–204. Wiley, New York (2009)
31.
Leue, S., Stefanescu, A., Wei, W.: An AsmL semantics for dynamic structures and run time schedulability in UML-RT. In: Paige, R.F., Meyer, B. (eds.) Proceedings of Objects, Components, Models and Patterns (TOOLS EUROPE 2008), Volume 11 of Lecture Notes in Business Information Processing, pp. 238–257. Springer, Berlin (2008)
32.
Li, X., Liu, Z., Jifeng, H.: A formal semantics of UML sequence diagrams. In: Proceedings of the 2004 Australian Software Engineering Conference, pp. 168–177 (2004)
33.
Merseguer, J., Bernardi, S., Campos, J., Donatelli, S.: A compositional semantics for UML state machines aimed at performance evaluation. In: Proceedings of the 6th International Workshop on Discrete Event Systems, pp. 295–302. IEEE Computer Society Press (2002)
34.
35.
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Parts I and II. Reports ECS-LFCS-89-85 and ECS-LFCS-89-86 86. Computer Science Dept., University of Edinburgh (1989)
36.
Möller, M.O., David, A., Yi, W.: Verification of UML statechart with real-time extensions. In: Fundamental Approaches to Software Engineering (FASE’2002), Volume 2306 of LNCS, pp. 218–232. Springer, Berlin (2003)
37.
Mrowka, R., Szmuc, T.: UML Statecharts Compositional Semantics in LOTOS. In: 2008 International Symposium on Parallel and Distributed Computing, pp. 459–463. IEEE Computer Society Press (2008)
38.
Muthiayen, D.: Real-Time Reactive System Development: A Formal Approach Based on UML and PVS. PhD thesis. Concordia University (2000)
39.
Ng, M.Y., Butler, M.: Towards formalizing UML state diagrams in CSP. In: Proceedings of SEFM’03, pp. 138–147. IEEE Computer Society (2003)
40.
41.
42.
43.
44.
45.
Paltor, I.: The Semantics of UML State Machines. Technical report (1999)
46.
Posse, E.: Modelling and Simulation of Dynamic Structure, Discrete-Event Systems. Ph.D. Thesis. School of Computer Science, McGill University (2008)
47.
48.
49.
Posse, E., Dingel, J.: kiltera: a language for timed, event-driven, mobile and distributed simulation. In: Proceedings of the 14th IEEE/ACM International Symposium on Distributed Simulation and Real Time Applications (DS-RT 2010) (2010)
50.
Posse, E., Dingel, J.: Theory and implementation of a real-time extension to the \(\pi \)-calculus. In: Proceedings of the International Conference on Formal Techniques for Distributed Systems (FMOODS & FORTE’10), LNCS (2010)
51.
Posse, E., Vangheluwe, H.: kiltera: a simulation language for timed, dynamic structure systems. In: Proceedings of the 40th Annual Simulation Symposium (ANSS’07) (2007)
52.
Ramos, R., Sampaio, A., Mota, A.: A semantics for UML-RT active classes via mapping into Circus. In: Proceedings of the International Conference on Formal Methods for Open Object-Based Distributed Systems FMOODS’05, Volume 3535 of LNCS, pp. 99–114. Springer, Berlin (2005)
53.
SAE International: Architecture Analysis & Design Language (AADL). SAE Standard AS5506b, 10 September (2012)
54.
Selic, B.: Using UML for modeling complex real-time systems. In: Mueller, F., Bestavros, A. (eds.) Languages, Compilers, and Tools for Embedded Systems (LCTES’98), Volume 1474 of LNCS, pp. 250–260. Springer, Berlin (1998)
55.
Selic, B.: Personal Communication, 1 February (2012)
56.
Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object Oriented Modeling. Wiley, New York (1994)MATH
57.
Selic, B., Rumbaugh, J.: Using UML for Modeling Complex Real-Time Systems. Whitepaper, Rational Software Corp (1998)
58.
Shankar, S., Asa, S.: Formal semantics of UML with real-time constructs. In: UML, Volume 2863 of LNCS, pp. 60–75. Springer, Berlin (2003)
59.
Störrle, H., Hausmann, J.H.: Towards a formal semantics of UML 2.0 activities. In: Proceedings German Software Engineering Conference, Volume 65 of LNI, pp. 117–128 (2005)
60.
von der Beeck, M.: A structured operational semantics for UML-statecharts. SoSyM 1(2), 130–141 (2002)
61.
von der Beeck, M.: A formal semantics of UML-RT. In: Proceedings of MoDELS’06, pp. 768–782 (2006)
62.
Yeung, W.L., Leung, K.R.P.H., Wang, J., Dong, W.: Improvements towards formalizing UML state diagrams in CSP. In: Proceedings of APSEC-’05, pp. 176–184. IEEE Computer Society (2005)
63.
Zeigler, B.P., Praehofer, H., Kim, T.G.: Theory of Modeling and Simulation, 1st edn. Academic Press, New York (1976)
64.
Zeigler, B.P., Praehofer, H., Kim, T.G.: Theory of Modeling and Simulation, 2nd edn. Academic Press, New York (2000)
65.
Zhang, T., Huang, S., Huang, H.: An operational semantics for UML RT-statechart in model checking context. In: Proceedings of the 4th International Conference on Internet Computing for Science and Engineering (ICICSE), pp. 12–18 (2009)
Metadata
Title
An executable formal semantics for UML-RT
Authors
Ernesto Posse
Juergen Dingel
Publication date
20-02-2014
Publisher
Springer Berlin Heidelberg
Published in
Software and Systems Modeling / Issue 1/2016
Print ISSN: 1619-1366
Electronic ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-014-0399-z

Other articles of this Issue 1/2016

Software and Systems Modeling 1/2016 Go to the issue

Regular Paper

Evaluating the appropriateness of the BPMN 2.0 standard for modeling service choreographies: using an extended quality framework

Regular Paper

Goal-oriented modeling and verification of feature-oriented product lines

Regular Paper

Synthesizing object life cycles from business process models

Regular Paper

SAMM: an architecture modeling methodology for ship command and control systems

Industry Voice

Cyber-physical systems challenges: a needs analysis for collaborating embedded software systems

Editorial

The 2015 “State of the Journal” report

Premium Partner

    Image Credits