Skip to main content
SpringerLink
Log in

Refining Mobile UML State Machines

  • Conference paper
Algebraic Methodology and Software Technology (AMAST 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3116))

Abstract

We study the semantics and refinement of mobile objects, considering an extension of core UML state machines by primitives that designate the location of objects and their moves within a network. Our contribution is twofold: first, we formalize the semantics of state machines in MTLA, an extension of Lamport’s Temporal Logic of Actions with spatial modalities. Second, we study refinement concepts for state machines that are semantically justified in MTLA.

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

Access this chapter

Log in via an institution
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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comp. Sci. 81(2), 253–284 (1991)

    Article  MathSciNet  Google Scholar 

  2. Baumeister, H., Koch, N., Kosiuczenko, P., Stevens, P., Wirsing, M.: UML for global computing. In: Priami, C. (ed.) GC 2003. LNCS, vol. 2874, pp. 1–24. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  3. Baumeister, H., Koch, N., Kosiuczenko, P., Wirsing, M.: Extending activity diagrams to model mobile systems. In: Aksit, M., Mezini, M., Unland, R. (eds.) NODe 2002. LNCS, vol. 2591, pp. 278–293. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). Inf. and Comp. 186(2), 194–235 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  5. Cardelli, L., Gordon, A.: Mobile ambients. Theor. Comp. Sci. 240, 177–213 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  6. Deiß, T.: An approach to the combination of formal description techniques: Statecharts and TLA. In: Araki, K., Galloway, A., Taguchi, K. (eds.) Integrated Formal Methods (IFM 1999), York, UK, pp. 231–250. Springer, Heidelberg (1999)

    Google Scholar 

  7. Harel, D.: Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming 8(3), 231–274 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  8. Kuhn, T.A., Oheimb., D.v.: Interacting state machines for mobility. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 698–718. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Lamport, L.: The Temporal Logic of Actions. ACM Trans. Prog. Lang. Syst. 16(3), 872–923 (1994)

    Article  Google Scholar 

  10. Latella, D., Massink, M., Baumeister, H., Wirsing, M.: Mobile UML statecharts with localities. Technical report 37, CNR ISTI, Pisa, Italy (2003)

    Google Scholar 

  11. Merz, S., Zappe, J., Wirsing, M.: A spatio-temporal logic for the specification and refinement of mobile systems. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 87–101. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Nicola, R.D., Ferrari, G., Pugliese, R.: Klaim: a kernel language for agents interaction and mobility. IEEE Trans. Software Eng. 24(5), 315–330 (1998)

    Article  Google Scholar 

  13. Nicola, R.D., Loreti, M.: A modal logic for Klaim. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 339–354. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  14. Object Management Group. Unified Modeling Language Specification, Version 1.5. Specification, OMG (2003), http://cgi.omg.org/cgi-bin/doc?formal/03-03-01

  15. Paech, B., Rumpe, B.: A new concept of refinement used for behaviour modelling with automata. In: Naftalin, M., Bertrán, M., Denvir, T. (eds.) FME 1994. LNCS, vol. 873, pp. 154–174. Springer, Heidelberg (1994)

    Google Scholar 

  16. Scholz, P.: A refinement calculus for Statecharts. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 285–301. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  17. Schrefl, M., Stumptner, M.: Behavior-consistent specialization of object life cycles. ACM Trans. Software Eng. Meth. 11(1), 92–148 (2002)

    Article  Google Scholar 

  18. von der Beeck, M.: Formalization of UML-statecharts. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, pp. 406–421. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Ludwig-Maximilians-Universität München,  

    Alexander Knapp & Martin Wirsing

  2. INRIA Lorraine, LORIA, Nancy

    Stephan Merz

Authors
  1. Alexander Knapp
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stephan Merz
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Martin Wirsing
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Stirling, FK9 4LA, Stirling, UK

    Charles Rattray

  2. University of Stirling, FK9 4LA, Stirling

    Savitri Maharaj

  3. Department of Computing Science and Mathematics, University of Stirling, FK9 4LA, Stirling, UK

    Carron Shankland

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Knapp, A., Merz, S., Wirsing, M. (2004). Refining Mobile UML State Machines. In: Rattray, C., Maharaj, S., Shankland, C. (eds) Algebraic Methodology and Software Technology. AMAST 2004. Lecture Notes in Computer Science, vol 3116. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27815-3_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-27815-3_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22381-8

  • Online ISBN: 978-3-540-27815-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation