Mobile Networks and Applications

, Volume 24, Issue 1, pp 134–144 | Cite as

Formal Verification of mCWQ Using Extended Hoare Logic

  • Wanling Xie
  • Huibiao ZhuEmail author
  • Xi Wu
  • Phan Cong Vinh


Node mobility, as one of the most important features of Wireless Sensor Networks (WSNs), may affect the reliability of communication links in the networks, leading to abnormalities and decreasing the quality of service provided by WSNs. The mCWQ calculus (i.e., CWQ calculus with mobility) is recently proposed to capture the feature of node mobility and increase the communication quality of WSNs. In this paper, we present a proof system for the mCWQ calculus to prove its correctness. Our specifications and verifications are based on Hoare Logic. In order to describe the timing of observable actions, we extend the assertion language with primitives. And terminating and non-terminating computations both can be described in our proof system. We also give some examples to illustrate the application of our proof system.


Hoare logic Node mobility mCWQ calculus 



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


  1. 1.
    Akyildiz IF, Su W, Sankarasubramaniam Y, Cayirci E (2002) Wireless sensor networks: a survey. Comput Netw 38(4):393–422CrossRefGoogle Scholar
  2. 2.
    Apt KR, de Boer FS, Olderog E (2009) Verification of sequential and concurrent programs. Texts in computer science. SpringerGoogle Scholar
  3. 3.
    Arthan R, Martin U, Oliva P (2013) A hoare logic for linear systems. Formal Asp Comput 25(3):345–363MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Barthe G, Gaboardi M, Arias EJG, Hsu J, Kunz C, Strub P (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
  5. 5.
    Bergstra JA, Klop JW (1984) Process algebra for synchronous communication. Inf Control 60(1-3):109–137MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    de Boer FS (2002) A hoare logic for dynamic networks of asynchronously communicating deterministic processes. Theor Comput Sci 274(1-2):3–41MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Camp T, Boleng J, Davies V (2002) A survey of mobility models for ad hoc network research. Wirel Commun Mob Comput 2(5):483–502CrossRefGoogle Scholar
  8. 8.
    Duran A, Cavalcanti A, Sampaio A (2010) An algebraic approach to the design of compilers for object-oriented languages. Formal Asp Comput 22(5):489–535CrossRefzbMATHGoogle Scholar
  9. 9.
    Ene C, Muntean T (2001) A broadcast-based calculus for communicating systems. In: Proceedings of the 15th international parallel & distributed processing symposium (IPDPS-01). San Francisco, CA, April 23–27, 2001, p 149Google Scholar
  10. 10.
    Fehnker A, van Glabbeek RJ, Höfner P, McIver A, Portmann M, Tan WL (2012) A process algebra for wireless mesh networks. In: Programming languages and systems - 21st European symposium on programming, ESOP 2012. Held as Part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, pp 295–315Google Scholar
  11. 11.
    Ghassemi F, Fokkink W, Movaghar A (2008) Restricted broadcast process theory. In: Sixth IEEE International conference on software engineering and formal methods, SEFM 2008. Cape Town, South Africa, 10-14 November 2008, pp 345–354Google Scholar
  12. 12.
    Godskesen JC (2007) A calculus for mobile ad hoc networks. In: Coordination models and languages, 9th international conference, coordination 2007. Paphos, Cyprus, June 6-8, 2007, Proceedings, pp 132–150Google Scholar
  13. 13.
    Godskesen JC, Nanz S (2009) Mobility models and behavioural equivalence for wireless networks. In: Coordination models and languages, 11th international conference, coordination 2009. Lisboa, Portugal, June 9-12, 2009. Proceedings, pp 106–122Google Scholar
  14. 14.
    He J (1994) Provably correct systems: modelling of communication languages and design of optimized compilers. The McGraw-Hill International Series in Software EngineeringGoogle Scholar
  15. 15.
    He J, Hoare CAR (1993) From algebra to operational semantics. Inf Process Lett 45(2):75–80MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    He J, Zhao X (2016) Reasoning about actions with loops via hoare logic. Front Comput Sci 10(5):870–888CrossRefGoogle Scholar
  17. 17.
    Hennessy M (1988) Algebraic theory of processes. MIT Press series in the foundations of computing, MIT PressGoogle Scholar
  18. 18.
    Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–580CrossRefzbMATHGoogle Scholar
  19. 19.
    Hoare CAR (1985) Communicating sequential processes. Prentice-HallGoogle Scholar
  20. 20.
    Hoare CAR, He J (1998) Unifying theories of programming. Prentice Hall International Series in Computer ScienceGoogle Scholar
  21. 21.
    Hoare CAR, Hayes IJ, He J, Morgan C, Roscoe AW, Sanders JW, Sørensen IH, Spivey JM, Sufrin B (1987) Laws of programming. Commun ACM 30(8):672–686MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Hoare CAR, He J, Sampaio A (1993) Normal form approach to compiler design. Acta Inf 30(8):701–739MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    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–149Google Scholar
  24. 24.
    Hoare T, van Staden S (2012) In praise of algebra. Formal Asp Comput 24(4-6):423–431MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    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–290Google Scholar
  26. 26.
    Hooman J (1994) Extending hoare logic to real-time. Formal Asp Comput 6(6A):801–826CrossRefzbMATHGoogle Scholar
  27. 27.
    Lanese I, Sangiorgi D (2010) An operational semantics for a calculus for wireless systems. Theor Comput Sci 411(19):1928–1948MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Lee EA (2015) Architectural support for cyber-physical systems. In: Proceedings of the twentieth international conference on architectural support for programming languages and operating systems, ASPLOS ’15. Istanbul, Turkey, March 14-18, 2015, p 1Google Scholar
  29. 29.
    Luo C, Qin S, Qiu Z (2008) Verifying bpel-like programs with hoare logic. Front Comput Sci Chin 2 (4):344–356CrossRefGoogle Scholar
  30. 30.
    Merro M (2009) An observational theory for mobile ad hoc networks (full version). Inf Comput 207(2):194–208MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Merro M, Ballardin F, Sibilio E (2011) A timed calculus for wireless systems. Theor Comput Sci 412 (47):6585–6611MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Milner R (1980) A calculus of communicating systems, lecture notes in computer science, vol 92. SpringerGoogle Scholar
  33. 33.
    Milner R (1999) Communicating and mobile systems - the Pi-calculus. Cambridge University PressGoogle Scholar
  34. 34.
    Nanz S, Hankin C (2006) Formal security analysis for ad-hoc networks. Electr Notes Theor Comput Sci 142:195–213CrossRefzbMATHGoogle Scholar
  35. 35.
    Nielson HR, Nielson F, Vigo R (2012) A calculus for quality. In: Formal aspects of component software, 9th international symposium, FACS 2012. Mountain View, CA, USA, September 12-14, 2012. Revised Selected Papers, pp 188–204Google Scholar
  36. 36.
    O’Hearn PW (2007) Resources, concurrency, and local reasoning. Theor Comput Sci 375(1-3):271–307MathSciNetCrossRefzbMATHGoogle Scholar
  37. 37.
    Perkins CE (1999) Belding-Royer EM Ad-hoc on-demand distance vector routing. In: 2nd Workshop on mobile computing systems and applications (WMCSA ’99), February 25-26, 1999. New Orleans, LA, USA, pp 90-100Google Scholar
  38. 38.
    Plotkin GD (2004) A structural approach to operational semantics. J Log Algebr Program 60-61:17–139MathSciNetCrossRefzbMATHGoogle Scholar
  39. 39.
    Prasad KVS (1995) A calculus of broadcasting systems. Sci Comput Program 25(2-3):285–327MathSciNetCrossRefGoogle Scholar
  40. 40.
    Rappaport TS (1996) Wireless communications - principles and practice. Prentice HallGoogle Scholar
  41. 41.
    Santi P (2005) Topology control in wireless ad hoc and sensor networks. ACM Comput Surv 37(2):164–194MathSciNetCrossRefGoogle Scholar
  42. 42.
    Song L, Godskesen JC (2010) Probabilistic mobility models for mobile and wireless networks. In: Theoretical computer science - 6th IFIP TC 1/WG 2.2 international conference, TCS 2010, Held as Part of WCC 2010, Brisbane, Australia, September 20-23, 2010. Proceedings, pp 86–100Google Scholar
  43. 43.
    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
  44. 44.
    Wu X, Zhu H (2015) A calculus for wireless sensor networks from quality perspective. In: 16th IEEE International symposium on high assurance systems engineering, HASE 2015, Daytona Beach, FL, USA, January 8-10, 2015, pp 223–231Google Scholar
  45. 45.
    Wu X, Zhao Y, Zhu H (2016) Integrating a calculus with mobility and quality for wireless sensor networks. In: 17th IEEE International symposium on high assurance systems engineering, HASE 2016, Orlando, FL, USA, January 7-9, 2016, pp 220–227Google Scholar
  46. 46.
    Xie W, Wu X, Zhu H, Lu G, Liu A (2017) A proof system for mCWQ. In: Proc. COMPSAC 2017: 41st IEEE computer society signature conference on computers, software and applications, pp 45–50Google Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Shanghai Key Laboratory of Trustworthy Computing, School of Computer Science and Software EngineeringEast China Normal UniversityShanghaiChina
  2. 2.School of ITEEThe University of QueenslandBrisbaneAustralia
  3. 3.Nguyen Tat Thanh UniversityHo Chi Minh CityVietnam

Personalised recommendations