UTP Semantics for rTiMo

  • Wanling XieEmail author
  • Shuangqing Xiang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10134)


rTiMo is a real-time version of TiMo (Timed Mobility), which is a process algebra for mobile distributed systems. In this paper, we investigate the denotational semantics for rTiMo. A trace variable tr is introduced to record the communications among processes as well as the location where the communication action takes place. Based on the formalized model, we study a set of algebraic laws, especially the laws about the migration and communication with real-time constraints. In order to facilitate the algebraic reasoning about the parallel expansion laws, we enrich rTiMo with a form of \(guarded \ choice\). This enables us to convert every parallel construct to a guarded choice.


Migration Process Output Process Semantic Model Parallel Composition Process Algebra 
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.



This work was partly supported by the Danish National Research Foundation and the National Natural Science Foundation of China (Grant No. 61361136002) for the Danish-Chinese Center for Cyber Physical Systems. It was also supported by National Natural Science Foundation of China (Grant No. 61321064) and Shanghai Collaborative Innovation Center of Trustworthy Software for Internet of Things (No. ZF1213).


  1. 1.
    Lakos, C.A.: A Petri net view of mobility. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 174–188. Springer, Heidelberg (2005). doi: 10.1007/11562436_14 CrossRefGoogle Scholar
  2. 2.
    Ma, L., Tsai, J.J.P.: Formal modeling and analysis of a secure mobile-agent system. IEEE Trans. Syst. Man Cybern. Part A 38(1), 180–196 (2008)CrossRefGoogle Scholar
  3. 3.
    Lakos, C.: Modelling mobile IP with mobile petri nets. In: Jensen, K., Billington, J., Koutny, M. (eds.) ToPNoC III. LNCS, vol. 5800, pp. 127–158. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-04856-2_6 CrossRefGoogle Scholar
  4. 4.
    Braghin, C., Sharygina, N., Barone-Adesi, K.: A model checking-based approach for security policy verification of mobile systems. Formal Asp. Comput. 23(5), 627–648 (2011)CrossRefzbMATHGoogle Scholar
  5. 5.
    Ciobanu, G., Koutny, M.: Timed mobility in process algebra and Petri nets. J. Log. Algebr. Program. 80(7), 377–391 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Aman, B., Ciobanu, G.: Real-time migration properties of rTiMo verified in uppaal. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 31–45. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-40561-7_3 CrossRefGoogle Scholar
  7. 7.
    Ciobanu, G., Koutny, M., Steggles, L.J.: Strategy based semantics for mobility with time and access permissions. Formal Asp. Comput. 27(3), 525–549 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Aman, B., Ciobanu, G.: Verification of bounded real-time distributed systems with mobility. In: Proceedings of the 9th Workshop on Verification and Evaluation of Computer and Communication Systems, VECoS 2015, Bucharest, Romania, September 10–11, pp. 109–120 (2015)Google Scholar
  9. 9.
    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). doi: 10.1007/978-3-642-21437-0_23 CrossRefGoogle Scholar
  10. 10.
    Ciobanu, G., Juravle, C.: Flexible software architecture and language for mobile agents. Concurrency Comput.: Pract. Experience 24(6), 559–571 (2012)CrossRefGoogle Scholar
  11. 11.
    Ciobanu, G., Koutny, M.: Pertimo: a model of spatial migration with safe access permissions. Comput. J. 58(5), 1041–1060 (2015)CrossRefGoogle Scholar
  12. 12.
    Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60–61, 17–139 (2004)MathSciNetzbMATHGoogle Scholar
  13. 13.
    Hoare, C.A.R., Hayes, I.J., He, J., Morgan, C., Roscoe, A.W., Sanders, J.W., Sørensen, I.H., Spivey, J.M., Sufrin, B.: Laws of programming. Commun. ACM 30(8), 672–686 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Hoare, C.A.R., He, J.: Unifying Theories of Programming. International Series in Computer Science. Prentice Hall, Upper Saddle River (1998)zbMATHGoogle Scholar
  15. 15.
    He, J.: Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers. International Series in Software Engineering. The McGraw-Hill, New York City (1994)CrossRefGoogle Scholar
  16. 16.
    Hoare, C.A.R., He, J., Sampaio, A.: Normal form approach to compiler design. Acta Inf. 30(8), 701–739 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Duran, A., Cavalcanti, A., Sampaio, A.: An algebraic approach to the design of compilers for object-oriented languages. Formal Asp. Comput. 22(5), 489–535 (2010)CrossRefzbMATHGoogle Scholar
  18. 18.
    Zhu, H., He, J., Qin, S., Brooke, P.J.: Denotational semantics and its algebraic derivation for an event-driven system-level language. Formal Asp. Comput. 27(1), 133–166 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Zhu, H., Yang, F., He, J., Bowen, J.P., Sanders, J.W., Qin, S.: Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language. J. Log. Algebr. Program. 81(1), 2–25 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Zhu, H., He, J., Li, J., Bowen, J.P.: Algebraic approach to linking the semantics of web services. ISSE 7(3), 209–224 (2011)Google Scholar
  21. 21.
    Apt, K.R., de Boer, F.S., Olderog, E.: Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer, Heidelberg (2009)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Shanghai Key Laboratory of Trustworthy Computing, School of Computer Science and Software EngineeringEast China Normal UniversityShanghaiChina

Personalised recommendations