Skip to main content

A Timed Mobility Semantics Based on Rewriting Strategies

  • Conference paper
Software Engineering and Formal Methods (SEFM 2012)

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

Included in the following conference series:

Abstract

We consider TiMo (Timed Mobility) which is a process algebra for prototyping software engineering applications supporting mobility and timing constraints. We provide an alternative semantics of TiMo using rewriting logic; in particular, we develop a rewriting logic model based on strategies to describe a maximal parallel computational step of a TiMo specification. This new semantical model is proved to be sound and complete w.r.t. to the original operational semantics which was based on negative premises. We implement the rewriting model within the strategy-based rewriting system Elan, and provide an example illustrating how a TiMo specification is executed and how a range of (behavioural) properties are analysed.

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

Access this chapter

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. Aman, B., Ciobanu, G.: Mobile Ambients with Timers and Types. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 50–63. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  2. Balland, E., Brauner, P., Kopetz, R., Moreau, P.-E., Reilles, A.: Tom: Piggybacking Rewriting on Java. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 36–47. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Berger, M.: Basic Theory of Reduction Congruence for Two Timed Asynchronous p-Calculi. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 115–130. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.–E., Ringeissen, C.: An overview of ELAN. In: Kirchner, C., Kirchner, H. (eds.) WRLA 1998 Electronic Notes in Theoretical Computer Science, vol. 15 (1998)

    Google Scholar 

  5. Borovanský, P., Kirchner, C., Kirchner, H., Ringeissen, C.: Rewriting with Strategies in ELAN: A Functional Semantics. International Journal of Foundations of Computer Science 12(1), 69–95 (2001)

    Article  MathSciNet  Google Scholar 

  6. Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.–E.: Elan from a rewriting logic point of view. Theoretical Computer Science 285(2), 155–185 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  7. Cardelli, L., Gordon, A.: Mobile Ambients. Theoretical Computer Science 240, 170–213 (2000)

    Article  MathSciNet  Google Scholar 

  8. Ciobanu, G., Koutny, M.: Modelling and Verification of Timed Interaction and Migration. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 215–229. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Ciobanu, G., Koutny, M.: Timed Mobility in Process Algebra and Petri Nets. Journal of Algebraic and Logic Programming 80(7), 377–391 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  10. Ciobanu, G., Koutny, M.: Timed Migration and Interaction with Access Permissions. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 293–307. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Ciobanu, G., Koutny, M., Steggles, L.J.: A Timed Mobility Semantics based on Rewriting Strategies. TR-1341. School of Computing Science, Newcastle University (2012)

    Google Scholar 

  12. Ciobanu, G., Prisacariu, C.: Timers for Distributed Systems. Electronic Notes in Theoretical Computer Science 164, 81–99 (2006)

    Article  Google Scholar 

  13. Clavel, M., et al.: Maude: Specification and Programming in Rewriting Logic. Theoretical Computer Science 285(2), 187–243 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  14. Corradini, F.: Absolute Versus Relative Time in Process Algebras. Information and Computation 156, 122–172 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  15. Hennessy, M.: A Distributed π-Calculus. Cambridge University Press (2007)

    Google Scholar 

  16. Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. Electronic Notes in Theoretical Computer Science 4, 190–225 (1996)

    Article  Google Scholar 

  17. Meinke, K., Tucker, J.V.: Universal Algebra. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. I: Mathematical Structures, pp. 189–411, Oxford University (1992)

    Google Scholar 

  18. Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(2), 73–155 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  19. Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press (1999)

    Google Scholar 

  20. Viry, P.: A rewriting implementation of pi-calculus. Technical Report TR-96-30. Departimento di Informatica, Universit‘a di Pisa, 26 (1996)

    Google Scholar 

  21. Visser, E.: Stratego: A Language for Program Transformation Based on Rewriting Strategies. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 357–361. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ciobanu, G., Koutny, M., Steggles, J. (2012). A Timed Mobility Semantics Based on Rewriting Strategies. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds) Software Engineering and Formal Methods. SEFM 2012. Lecture Notes in Computer Science, vol 7504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33826-7_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33826-7_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33825-0

  • Online ISBN: 978-3-642-33826-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics