Formal Aspects of Computing

, Volume 30, Issue 6, pp 713–738 | Cite as

A UTP approach for rTiMo

  • Wanling Xie
  • Shuangqing Xiang
  • Huibiao ZhuEmail author
Original Article


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 can enable us to convert every parallel program to the guarded choice form. Moreover, we also provide a set of proof rules, which can be used to verify the correctness and real-time properties of programs.


rTiMo Mobile systems UTP semantics Hoare logic 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. AC13.
    Aman B, Ciobanu G (2013) Real-time migration properties of rtimo verified in Uppaal. In: 11th international conference, SEFM 2013 software engineering and formal methods, Madrid, Spain, September 25–27, 2013, proceedings, pp. 31–45Google Scholar
  2. AC15a.
    Aman B, Ciobanu G(2015) Timed mobility and timed communication for critical systems. In: Formal methods for industrial critical systems-20th international workshop, FMICS 2015, Oslo, Norway, June 22–23, 2015 proceedings, pp. 146–161CrossRefGoogle Scholar
  3. AC15b.
    Aman B, Ciobanu G(2015) 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, 2015, pp 109–120Google Scholar
  4. AdBO09.
    Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of sequential and concurrent programs. Springer, Texts in computer science (2009)CrossRefGoogle Scholar
  5. AMO13.
    Arthan, R., Martin, U., Oliva, P.: A Hoare Logic for linear systems. Formal Asp Comput 25(3), 345–363 (2013)MathSciNetCrossRefGoogle Scholar
  6. BGA+14.
    Barthe G, Gaboardi M, Arias EJG, Hsu J, Kunz C, Strub PY (2014) Proving differential privacy in Hoare logic. In:IEEE 27th computer security foundations symposium, CSF 2014, Vienna, Austria, 19–22 July, 2014, pp. 411–424Google Scholar
  7. BSB11.
    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)CrossRefGoogle Scholar
  8. CG00.
    Cardelli, L., Gordon, A.D.: Mobile ambients. Theor Comput Sci 240(1), 177–213 (2000)MathSciNetCrossRefGoogle Scholar
  9. CJ12.
    Ciobanu, G., Juravle, C.: Flexible software architecture and language for mobile agents. Concurrency and computation: practice and experience 24(6), 559–571 (2012)CrossRefGoogle Scholar
  10. CK11a.
    Ciobanu G, Koutny M (2011) Timed migration and interaction with access permissions. In:FM 2011: Formal methods-17th international symposium on formal methods, Limerick, Ireland, June 20-24, 2011, proceedings, pp 293–307Google Scholar
  11. CK11b.
    Ciobanu, G., Koutny, M.: Timed mobility in process algebra and Petri nets. J Log Algebr Program 80(7), 377–391 (2011)MathSciNetCrossRefGoogle Scholar
  12. CK15.
    Ciobanu, G., Koutny, M.: Pertimo: A model of spatial migration with safe access permissions. Comput J 58(5), 1041–1060 (2015)CrossRefGoogle Scholar
  13. CKS15.
    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)MathSciNetCrossRefGoogle Scholar
  14. CP95.
    Christensen S, Petrucci L (1995) Modular state space analysis of coloured Petri nets. In:16th international conference application and theory of petri nets 1995, Turin, Italy, June 26–30, 1995, proceedings, pp 201–217Google Scholar
  15. CP00.
    Christensen, S., Petrucci, L.: Modular analysis of Petri nets. Comput J 43(3), 224–242 (2000)CrossRefGoogle Scholar
  16. CWW13.
    Cavalcanti, A., Wellings, A.J., Woodcock, J.: The safety-critical java memory model formalised. Formal Asp Comput 25(1), 37–57 (2013)MathSciNetCrossRefGoogle Scholar
  17. dB02.
    de Boer, Frank S.: A Hoare logic for dynamic networks of asynchronously communicating deterministic processes. Theor Comput Sci 274(1–2), 3–41 (2002)MathSciNetCrossRefGoogle Scholar
  18. DCS10.
    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)CrossRefGoogle Scholar
  19. DGJP04.
    Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled markov processes. Theor Comput Sci 318(3), 323–354 (2004)MathSciNetCrossRefGoogle Scholar
  20. FGH+14.
    Ferreira, J.F., Gherghina, C., He, G., Qin, S., Chin, W.-N.: Automated verification of the FreeRTOS scheduler in Hip/Sleek. STTT 16(4), 381–397 (2014)CrossRefGoogle Scholar
  21. Gol96.
    Golze, U.: VLSI chip design with the hardware description language VERILOG-an introduction based on a large RISC processor design. Springer, Berlin (1996)CrossRefGoogle Scholar
  22. Gor95.
    Gordon Michael JC (1995) The semantic challenge of Verilog HDL. In: Proceedings, 10th annual IEEE symposium on logic in computer science, San Diego, California, USA, June 26-29, 1995, pp. 136–145Google Scholar
  23. He94.
    He J (1994) Provably correct systems: modelling of communication languages and design of optimized compilers. The McGraw-Hill international series in software engineeringGoogle Scholar
  24. He16.
    He J (2016) A new roadmap for linking theories of programming. In: Unifying theories of programming-6th international symposium, UTP 2016, Reykjavik, Iceland, June 4–5, 2016, Revised Selected Papers, pp 26–43Google Scholar
  25. Hen88.
    Hennessy, M.: Algebraic theory of processes. MIT Press series in the foundations of computing, MIT Press (1988)zbMATHGoogle Scholar
  26. HH93.
    He, J., Hoare, C.A.R.: From algebra to operational semantics. Inf Process Lett 45(2), 75–80 (1993)MathSciNetCrossRefGoogle Scholar
  27. HH98.
    Hoare CAR, He J (1998) Unifying Theories of Programming. Prentice Hall International Series in Computer ScienceGoogle Scholar
  28. HHH+87.
    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)MathSciNetCrossRefGoogle Scholar
  29. HHS93.
    Hoare, C.A.R., He, J., Sampaio, A.: Normal form approach to compiler design. Acta Inf 30(8), 701–739 (1993)MathSciNetCrossRefGoogle Scholar
  30. HHZ+15.
    Huang, Y., He, J., Zhu, H., Zhao, Y., Shi, J., Qin, S.: Semantic theories of programs with nested interrupts. Front Comput Sci. 9(3), 331–345 (2015)CrossRefGoogle Scholar
  31. Hoa69.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun ACM 12(10), 576–580 (1969)CrossRefGoogle Scholar
  32. Hoa85.
    Hoare CAR (1985) Communicating sequential processes. Prentice-Hall,Google Scholar
  33. Hoa13.
    Hoare T (2013) Unifying semantics for concurrent programming. In:Computation, logic, games, and quantum foundations. the many facets of samson abramsky-essays dedicated to samson abramsky on the occasion of his 60th Birthday, pp 139–149CrossRefGoogle Scholar
  34. Hoo91.
    Hooman J (1991) Compositional verification of real-time systems using extended hoare triples. In: Real-time: theory in practice, REX workshop, Mook, The Netherlands, June 3–7, 1991, proceedings, pp 252–290CrossRefGoogle Scholar
  35. Hoo94.
    Hooman, J.: Extending Hoare Logic to real-time. Formal Asp Comput 6(6A), 801–826 (1994)CrossRefGoogle Scholar
  36. HSM97.
    He, J., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Sci Comput Program 28(2–3), 171–192 (1997)MathSciNetzbMATHGoogle Scholar
  37. HvS12.
    Hoare, T., van Staden, S.: In praise of algebra. Formal Asp Comput 24(4–6), 423–431 (2012)MathSciNetCrossRefGoogle Scholar
  38. HvSM+16.
    Hoare, T., van Staden, S., Möller, B., Struth, G., Zhu, H.: Developments in concurrent Kleene algebra. J Log Algebr Methods Program 85(4), 617–636 (2016)MathSciNetCrossRefGoogle Scholar
  39. HZ16.
    He, J., Zhao, X.: Reasoning about actions with loops via Hoare logic. Front Comput Sci 10(5), 870–888 (2016)CrossRefGoogle Scholar
  40. Lak05.
    Lakos C (2005) A Petri net view of mobility. In: Formal techniques for networked and distributed systems-FORTE 2005, 25th IFIP WG 6.1 international conference, Taipei, Taiwan, October 2–5, 2005, proceedings, pp 174–188CrossRefGoogle Scholar
  41. Lak09.
    Lakos C (2009) Modelling mobile IP with mobile Petri nets.Transactions on petri nets and other models of concurrency III. Lecture notes in computer science 5800, Springer 2009, ISBN 978-3-642-04854-8, 3:127–158Google Scholar
  42. LQQ08.
    Luo, C., Qin, S., Qiu, Z.: Verifying BPEL-like programs with Hoare Logic. Front Comput Sci China 2(4), 344–356 (2008)CrossRefGoogle Scholar
  43. Mäk02.
    Mäkelä M (2002) Maria: modular reachability analyser for algebraic system nets. In: Applications and theory of Petri nets 2002, 23rd international conference, ICATPN 2002, Adelaide, Australia, June 24-30, 2002, proceedings, pp 434–444CrossRefGoogle Scholar
  44. Mil80.
    Milner R (1980) A calculus of communicating systems  (Lecture notes in computer science), vol 92. SpringerGoogle Scholar
  45. Mil93.
    Milner, R.: Elements of interaction-turing award lecture. Commun ACM 36(1), 78–89 (1993)MathSciNetCrossRefGoogle Scholar
  46. Mil99.
    Milner, R.: Communicating and mobile systems-the Pi-calculus. Cambridge University Press, Cambridge (1999)zbMATHGoogle Scholar
  47. MM05.
    McIver, A., Morgan, C.: Abstraction and refinement in probabilistic systems. SIGMETRICS Perform Eval Rev 32(4), 41–47 (2005)CrossRefGoogle Scholar
  48. MT08.
    Ma, L., Tsai, J.J.P.: Formal modeling and analysis of a secure mobile-agent system. IEEE Trans Syst Man and Cyber Part A 38(1), 180–196 (2008)CrossRefGoogle Scholar
  49. O’H07.
    O'Hearn, P.W.: Resources, concurrency, and local reasoning. Theor Comput Sci 375(1–3), 271–307 (2007)MathSciNetCrossRefGoogle Scholar
  50. Pau94.
    Paulson LC (1994) Isabelle-A Generic theorem prover (with a contribution by T. Nipkow), volume 828 of Lecture notes in computer science. SpringerGoogle Scholar
  51. Plo04.
    Plotkin, G.D.: A structural approach to operational semantics. J Log Algebr Program 60–61, 17–139 (2004)MathSciNetzbMATHGoogle Scholar
  52. Pra90.
    Vaughan RP (1990) Action logic and pure induction. In: Logics in AI, European workshop, JELIA '90, Amsterdam, The Netherlands, September 10–14, 1990, proceedings, pp 97–120Google Scholar
  53. QHL+14.
    Qin, S., He, G., Luo, C., Chin, W.-N., Yang, H.: Automatically refining partial specifications for heap-manipulating programs. Sci Comput Program 82, 56–76 (2014)CrossRefGoogle Scholar
  54. Shi09.
    Shi L (2009) Comparative studies, formal semantics and PVS encoding of CSP\(\#\). PhD thesis, East China Normal University,ChinaGoogle Scholar
  55. SLDC09.
    Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating specification and programs for system modeling and verification. TASE 2009, third IEEE international symposium on theoretical aspects of software engineering, 29–31 July 2009, pp. 127–135. Tianjin, China (2009)CrossRefGoogle Scholar
  56. Sto79.
    Stoy JE (1979) Foundations of denotational semantics. In:Abstract software specifications, 1979 Copenhagen Winter School, January 22 –February 2, 1979, proceedings, pp 43–99Google Scholar
  57. SZL+18.
    Shi L, Zhao Y, Liu Y, Sun J, Dong JS, Qin S (2018) A UTP semantics for communicating processes with shared variables and its formal encoding in PVS.Formal Asp ComputGoogle Scholar
  58. Tar55.
    Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5(2), 285–309 (1955)MathSciNetCrossRefGoogle Scholar
  59. Val98.
    Valk R (1998) Petri nets as token objects: An introduction to elementary object nets. In:19th international conference application and theory of petri nets 1998 ICATPN '98, Lisbon, Portugal, June 22-26, 1998, proceedings, pp 1–25Google Scholar
  60. vO01.
    von Oheimb, D.: Hoare logic for java in Isabelle/HOL. Concurr Comput Pract Exp. 13(13), 1173–1214 (2001)CrossRefGoogle Scholar
  61. Wat91.
    Watt, D.A.: Programming language syntax and semantics. Prentice Hall, Prentice Hall International series in computer science (1991)zbMATHGoogle Scholar
  62. XX16.
    Xie W, Xiang S (2016) UTP semantics for rTiMo. In Unifying theories of programming-6th international symposium, UTP 2016, Reykjavik, Iceland, June 4–5, 2016, Revised Selected Papers, pp. 176–196Google Scholar
  63. ZHB08.
    Zhu, H., He, J., Bowen, J.P.: From algebraic semantics to denotational semantics for Verilog. ISSE 4(4), 341–360 (2008)zbMATHGoogle Scholar
  64. ZHLB11.
    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
  65. ZHQB15.
    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)MathSciNetCrossRefGoogle Scholar
  66. Zhu05.
    Zhu H (2005)Linking the semantics of a multithreaded discrete event simulation language. PhD thesis, London South Bank University UKGoogle Scholar
  67. ZYH+12.
    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)MathSciNetCrossRefGoogle Scholar
  68. ZZW+13.
    Zou L, Zhan N, Wang S, Fränzle M, Qin S (2013) Verifying Simulink diagrams via a hybrid hoare logic prover. In: Proceedings of the international conference on embedded software, EMSOFT 2013, Montreal, QC, Canada, September 29–Oct. 4, 2013, pp 9:1–9:10Google Scholar

Copyright information

© British Computer Society 2018

Authors and Affiliations

  1. 1.Shanghai Key Laboratory of Trustworthy Computing, MOE International Joint Laboratory of Trustworthy Software, International Research Center of Trustworthy SoftwareEast China Normal UniversityShanghaiChina
  2. 2.School of Computer Science and Software EngineeringShenzhen UniversityShenzhenChina

Personalised recommendations