Skip to main content

Refinement Patterns for Hierarchical UML State Machines

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5961))

Abstract

While the semantics of (labeled) transition systems and the relations between these are well understood, the same still needs to be achieved for UML 2.x state machines, because the UML standard is ambiguous and admits many semantics, which are often defined in terms of labeled transition systems.

A formal semantics for UML state machines with interlevel transitions and notions of refinement are described to enable the study of transformations, i.e., functions from state machines to state machines, and to establish the conditions under which these transformations are refinement steps. Many of these transformations are described and shown to be refinement steps. A language extension is finally proposed that help modelers to ensure that all transformations are indeed refinements.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8(3), 231–274 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  2. Harel, D., Gery, E.: Executable object modeling with Statecharts. Computer 30(7), 31–42 (1997)

    Article  Google Scholar 

  3. Selic, B., Gullekson, G., Ward, P.T.: Real-Time Object-Oriented Modeling. John Wiley & Sons, Inc., New York (1994)

    MATH  Google Scholar 

  4. Maraninchi, F., Rémond, Y.: Argos: an automaton-based synchronous language. Comp. Lang. 27(1/3), 61–92 (2001)

    Article  MATH  Google Scholar 

  5. OMG: UML 2.1.2 Superstructure Specification (November 2007), http://www.omg.org/cgi-bin/docs/formal/2007-11-02.pdf

  6. Fecher, H., Schönborn, J., Kyas, M., de Roever, W.P.: 29 new unclarities in the semantics of UML 2.0 state machines. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 52–65. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Latella, D., Majzik, I., Massink, M.: Towards a formal operational semantics of UML Statechart diagrams. In: Ciancarini, P., Gorrieri, R. (eds.) FMOODS, pp. 331–347. Kluwer Academic Publishers, Dordrecht (1999)

    Google Scholar 

  8. von der Beeck, M.: A structured operational semantics for UML-statecharts. Software and Systems Modeling 1(2), 130–141 (2002)

    Article  Google Scholar 

  9. Bianco, V.D., Lavazza, L., Mauri, M.: A formalization of UML Statecharts for real-time software modeling. In: The Sixth Biennal World Conference of Integrated Design Process Technology, IDPT 2002 (2002)

    Google Scholar 

  10. Jürjens, J.: Formal semantics of interacting uml subsystems. In: Jacobs, B., Rensink, A. (eds.) FMOODS, pp. 29–44. Kluwer Academic Publishers, Dordrecht (2002)

    Google Scholar 

  11. Börger, E., Cavarra, A., Riccobene, E.: Modeling the meaning of transitions from and to concurrent states in UML state machines. In: SAC, pp. 1086–1091. ACM Press, New York (2003)

    Google Scholar 

  12. Fecher, H., Schönborn, J.: UML 2.0 state machines: Complete formal semantics via core state machine. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 244–260. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  13. Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  14. Rumpe, B.: Formale Methodik des Entwurfs verteilter objektorientierter Systeme. Herbert Utz Verlag Wissenschaft (1997)

    Google Scholar 

  15. Meng, S., Naixiao, Z., Barbosa, L.S.: On semantics and refinement of UML Statecharts: A coalgebraic view. In: SEFM, pp. 164–173. IEEE, Los Alamitos (2004)

    Google Scholar 

  16. de Roever, W.P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol. 47. Cambridge University Press, Cambridge (1998)

    MATH  Google Scholar 

  17. Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)

    MATH  Google Scholar 

  18. van Glabbeek, R.J.: The linear time-branching time spectrum (extended abstract). In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990)

    Google Scholar 

  19. Reeve, G., Reeves, S.: Logic and refinement for charts. In: Estivill-Castro, V., Dobbie, G. (eds.) ACSC. CRPIT, vol. 48, pp. 13–23. Australian Computer Society (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schönborn, J., Kyas, M. (2010). Refinement Patterns for Hierarchical UML State Machines. In: Arbab, F., Sirjani, M. (eds) Fundamentals of Software Engineering. FSEN 2009. Lecture Notes in Computer Science, vol 5961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11623-0_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11623-0_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11622-3

  • Online ISBN: 978-3-642-11623-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics