Abstract
This paper extends the TiMo family by introducing a real-time version named rTiMo. The rTiMo processes are able to move between different locations of a distributed environment, and communicate locally with other processes. Real-time constraints are used to control migration and communication in a real-time distributed system. In order to verify several properties of complex mobile systems described in rTiMo, we establish a relationship between rTiMo networks and a class of timed safety automata. The relationship allows the verification of temporal properties of real-time migrating processes using Uppaal capabilities. In particular, we check whether certain configurations are reached, and that certain timing constraints hold for an entire complex evolution.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)
Aman, B., Ciobanu, G., Koutny, M.: Behavioural Equivalences over Migrating Processes with Timers. In: Giese, H., Rosu, G. (eds.) FMOODS/FORTE 2012. LNCS, vol. 7273, pp. 52–66. Springer, Heidelberg (2012)
Baeten, J.C.M., Bergstra, J.A.: Real Time Process Algebra. Journal of Formal Aspects of Computing Science 3(2), 142–188 (1991)
Baumann, J., Hohl, F., Radouniklis, N., Rothermel, K., Straβer, M.: Communication Concepts for Mobile Agent Systems. In: Rothermel, K., Popescu-Zeletin, R. (eds.) MA 1997. LNCS, vol. 1219, pp. 123–135. Springer, Heidelberg (1997)
Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Čerāns, K.: Decidability of Bisimulation Equivalences for Parallel Timer Processes. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 302–315. Springer, Heidelberg (1993)
Ciobanu, G., Juravle, C.: Flexible Software Architecture and Language for Mobile Agents. Concurrency and Computation: Practice and Experience 24, 559–571 (2012)
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 Logic and Algebraic Programming 80, 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., Prisacariu, C.: Timers for Distributed Systems. Electronic Notes in Theoretic Computer Science 164(3), 81–99 (2006)
Groote, J.F.: Transition System Specifications with Negative Premises. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 332–341. Springer, Heidelberg (1990)
Hennessy, M., Regan, T.: A Process Algebra for Timed Systems. Information and Computation 117, 221–239 (1995)
Hennessy, M.: A Distributed π-calculus. Cambridge University Press (2007)
Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Model Checking for Real-time Systems. Information and Computation 111, 192–224 (1994)
Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing Real-Time Systems Using UPPAAL. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 77–117. Springer, Heidelberg (2008)
Larsen, K.G., Petterson, P., Yi, W.: Uppaal in a Nutshell. International Journal on Software Tools for Technology Transfer 1(2), 134–152 (1997)
Milner, R.: Communicating and Mobile Systems: the π-calculus. Cambridge University Press (1999)
Moller, F., Tofts, C.: A Temporal Calculus of Communicating Systems. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 401–415. Springer, Heidelberg (1990)
Reed, G.M., Roscoe, A.W.: A Timed Model for Communicating Sequential Processes. Theoretical Computer Science 58(1-3), 249–261 (1988)
Yi, W., Pettersson, P., Daniels, M.: Automatic Verification of Real-time Communicating Systems by Constraint-solving. In: International Conference on Formal Description Techniques, pp. 223–238 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aman, B., Ciobanu, G. (2013). Real-Time Migration Properties of rTiMo Verified in Uppaal . In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds) Software Engineering and Formal Methods. SEFM 2013. Lecture Notes in Computer Science, vol 8137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40561-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-40561-7_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40560-0
Online ISBN: 978-3-642-40561-7
eBook Packages: Computer ScienceComputer Science (R0)