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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
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)
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)
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)
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)
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)
Cardelli, L., Gordon, A.: Mobile Ambients. Theoretical Computer Science 240, 170–213 (2000)
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)
Ciobanu, G., Koutny, M.: Timed Mobility in Process Algebra and Petri Nets. Journal of Algebraic and Logic Programming 80(7), 377–391 (2011)
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)
Ciobanu, G., Koutny, M., Steggles, L.J.: A Timed Mobility Semantics based on Rewriting Strategies. TR-1341. School of Computing Science, Newcastle University (2012)
Ciobanu, G., Prisacariu, C.: Timers for Distributed Systems. Electronic Notes in Theoretical Computer Science 164, 81–99 (2006)
Clavel, M., et al.: Maude: Specification and Programming in Rewriting Logic. Theoretical Computer Science 285(2), 187–243 (2002)
Corradini, F.: Absolute Versus Relative Time in Process Algebras. Information and Computation 156, 122–172 (2000)
Hennessy, M.: A Distributed π-Calculus. Cambridge University Press (2007)
MartÃ-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. Electronic Notes in Theoretical Computer Science 4, 190–225 (1996)
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)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(2), 73–155 (1992)
Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press (1999)
Viry, P.: A rewriting implementation of pi-calculus. Technical Report TR-96-30. Departimento di Informatica, Universit‘a di Pisa, 26 (1996)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)