Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Software and Systems Modeling
Erschienen in: Software and Systems Modeling 1/2016

20.02.2014 | Regular Paper

An executable formal semantics for UML-RT

verfasst von: Ernesto Posse, Juergen Dingel

Erschienen in: Software and Systems Modeling | Ausgabe 1/2016

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.
Vorheriger Artikel A profile and tool for modelling safety information with design information in SysML
Nächster Artikel Evaluating the appropriateness of the BPMN 2.0 standard for modeling service choreographies: using an extended quality framework

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
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.
 
Literatur
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)
Metadaten
Titel
An executable formal semantics for UML-RT
verfasst von
Ernesto Posse
Juergen Dingel
Publikationsdatum
20.02.2014
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 1/2016
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-014-0399-z

Weitere Artikel der Ausgabe 1/2016

Software and Systems Modeling 1/2016 Zur Ausgabe

Regular Paper

A profile and tool for modelling safety information with design information in SysML

Regular Paper

Synthesizing object life cycles from business process models

Regular Paper

Formalizing and appling compliance patterns for business process compliance

Industry Voice

Industry 4.0 as a Cyber-Physical System study

Regular Paper

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

Regular Paper

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

Premium Partner

    Bildnachweise