{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:22:57Z","timestamp":1772835777089,"version":"3.50.1"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2018,9,29]],"date-time":"2018-09-29T00:00:00Z","timestamp":1538179200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,9,29]],"date-time":"2018-09-29T00:00:00Z","timestamp":1538179200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mobile Netw Appl"],"published-print":{"date-parts":[[2019,2,15]]},"DOI":"10.1007\/s11036-018-1142-8","type":"journal-article","created":{"date-parts":[[2018,9,29]],"date-time":"2018-09-29T04:55:01Z","timestamp":1538196901000},"page":"134-144","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formal Verification of mCWQ Using Extended Hoare Logic"],"prefix":"10.1007","volume":"24","author":[{"given":"Wanling","family":"Xie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xi","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0797-0152","authenticated-orcid":false,"given":"Phan Cong","family":"Vinh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,29]]},"reference":[{"issue":"4","key":"1142_CR1","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1016\/S1389-1286(01)00302-4","volume":"38","author":"IF Akyildiz","year":"2002","unstructured":"Akyildiz IF, Su W, Sankarasubramaniam Y, Cayirci E (2002) Wireless sensor networks: a survey. Comput Netw 38(4):393\u2013422","journal-title":"Comput Netw"},{"key":"1142_CR2","doi-asserted-by":"crossref","unstructured":"Apt KR, de Boer FS, Olderog E (2009) Verification of sequential and concurrent programs. Texts in computer science. Springer","DOI":"10.1007\/978-1-84882-745-5"},{"issue":"3","key":"1142_CR3","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/s00165-011-0180-9","volume":"25","author":"R Arthan","year":"2013","unstructured":"Arthan R, Martin U, Oliva P (2013) A hoare logic for linear systems. Formal Asp Comput 25(3):345\u2013363","journal-title":"Formal Asp Comput"},{"key":"1142_CR4","doi-asserted-by":"crossref","unstructured":"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\u2013424","DOI":"10.1109\/CSF.2014.36"},{"issue":"1-3","key":"1142_CR5","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","volume":"60","author":"JA Bergstra","year":"1984","unstructured":"Bergstra JA, Klop JW (1984) Process algebra for synchronous communication. Inf Control 60(1-3):109\u2013137","journal-title":"Inf Control"},{"issue":"1-2","key":"1142_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00304-2","volume":"274","author":"FS de Boer","year":"2002","unstructured":"de Boer FS (2002) A hoare logic for dynamic networks of asynchronously communicating deterministic processes. Theor Comput Sci 274(1-2):3\u201341","journal-title":"Theor Comput Sci"},{"issue":"5","key":"1142_CR7","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1002\/wcm.72","volume":"2","author":"T Camp","year":"2002","unstructured":"Camp T, Boleng J, Davies V (2002) A survey of mobility models for ad hoc network research. Wirel Commun Mob Comput 2(5):483\u2013502","journal-title":"Wirel Commun Mob Comput"},{"issue":"5","key":"1142_CR8","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/s00165-009-0124-9","volume":"22","author":"A Duran","year":"2010","unstructured":"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\u2013535","journal-title":"Formal Asp Comput"},{"key":"1142_CR9","unstructured":"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\u201327, 2001, p 149"},{"key":"1142_CR10","doi-asserted-by":"crossref","unstructured":"Fehnker A, van Glabbeek RJ, H\u00f6fner 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\u2013315","DOI":"10.1007\/978-3-642-28869-2_15"},{"key":"1142_CR11","doi-asserted-by":"crossref","unstructured":"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\u2013354","DOI":"10.1109\/SEFM.2008.25"},{"key":"1142_CR12","doi-asserted-by":"crossref","unstructured":"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\u2013150","DOI":"10.1007\/978-3-540-72794-1_8"},{"key":"1142_CR13","doi-asserted-by":"crossref","unstructured":"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\u2013122","DOI":"10.1007\/978-3-642-02053-7_6"},{"key":"1142_CR14","unstructured":"He J (1994) Provably correct systems: modelling of communication languages and design of optimized compilers. The McGraw-Hill International Series in Software Engineering"},{"issue":"2","key":"1142_CR15","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0020-0190(93)90219-Y","volume":"45","author":"J He","year":"1993","unstructured":"He J, Hoare CAR (1993) From algebra to operational semantics. Inf Process Lett 45(2):75\u201380","journal-title":"Inf Process Lett"},{"issue":"5","key":"1142_CR16","doi-asserted-by":"publisher","first-page":"870","DOI":"10.1007\/s11704-016-5158-6","volume":"10","author":"J He","year":"2016","unstructured":"He J, Zhao X (2016) Reasoning about actions with loops via hoare logic. Front Comput Sci 10(5):870\u2013888","journal-title":"Front Comput Sci"},{"key":"1142_CR17","unstructured":"Hennessy M (1988) Algebraic theory of processes. MIT Press series in the foundations of computing, MIT Press"},{"issue":"10","key":"1142_CR18","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580","journal-title":"Commun ACM"},{"key":"1142_CR19","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice-Hall","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"1142_CR20","doi-asserted-by":"crossref","unstructured":"Hoare CAR, He J (1998) Unifying theories of programming. Prentice Hall International Series in Computer Science","DOI":"10.1007\/BFb0002714"},{"issue":"8","key":"1142_CR21","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"CAR Hoare","year":"1987","unstructured":"Hoare CAR, Hayes IJ, He J, Morgan C, Roscoe AW, Sanders JW, S\u00f8rensen IH, Spivey JM, Sufrin B (1987) Laws of programming. Commun ACM 30(8):672\u2013686","journal-title":"Commun ACM"},{"issue":"8","key":"1142_CR22","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/BF01191809","volume":"30","author":"CAR Hoare","year":"1993","unstructured":"Hoare CAR, He J, Sampaio A (1993) Normal form approach to compiler design. Acta Inf 30(8):701\u2013739","journal-title":"Acta Inf"},{"key":"1142_CR23","doi-asserted-by":"crossref","unstructured":"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\u2013149","DOI":"10.1007\/978-3-642-38164-5_10"},{"issue":"4-6","key":"1142_CR24","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s00165-012-0249-0","volume":"24","author":"T Hoare","year":"2012","unstructured":"Hoare T, van Staden S (2012) In praise of algebra. Formal Asp Comput 24(4-6):423\u2013431","journal-title":"Formal Asp Comput"},{"key":"1142_CR25","doi-asserted-by":"crossref","unstructured":"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\u20137, 1991, Proceedings, pp 252\u2013290","DOI":"10.1007\/BFb0031996"},{"issue":"6A","key":"1142_CR26","doi-asserted-by":"publisher","first-page":"801","DOI":"10.1007\/BF01213604","volume":"6","author":"J Hooman","year":"1994","unstructured":"Hooman J (1994) Extending hoare logic to real-time. Formal Asp Comput 6(6A):801\u2013826","journal-title":"Formal Asp Comput"},{"issue":"19","key":"1142_CR27","doi-asserted-by":"publisher","first-page":"1928","DOI":"10.1016\/j.tcs.2010.01.023","volume":"411","author":"I Lanese","year":"2010","unstructured":"Lanese I, Sangiorgi D (2010) An operational semantics for a calculus for wireless systems. Theor Comput Sci 411(19):1928\u20131948","journal-title":"Theor Comput Sci"},{"key":"1142_CR28","doi-asserted-by":"crossref","unstructured":"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 \u201915. Istanbul, Turkey, March 14-18, 2015, p 1","DOI":"10.1145\/2694344.2694375"},{"issue":"4","key":"1142_CR29","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/s11704-008-0039-2","volume":"2","author":"C Luo","year":"2008","unstructured":"Luo C, Qin S, Qiu Z (2008) Verifying bpel-like programs with hoare logic. Front Comput Sci Chin 2 (4):344\u2013356","journal-title":"Front Comput Sci Chin"},{"issue":"2","key":"1142_CR30","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/j.ic.2007.11.010","volume":"207","author":"M Merro","year":"2009","unstructured":"Merro M (2009) An observational theory for mobile ad hoc networks (full version). Inf Comput 207(2):194\u2013208","journal-title":"Inf Comput"},{"issue":"47","key":"1142_CR31","doi-asserted-by":"publisher","first-page":"6585","DOI":"10.1016\/j.tcs.2011.07.016","volume":"412","author":"M Merro","year":"2011","unstructured":"Merro M, Ballardin F, Sibilio E (2011) A timed calculus for wireless systems. Theor Comput Sci 412 (47):6585\u20136611","journal-title":"Theor Comput Sci"},{"key":"1142_CR32","doi-asserted-by":"crossref","unstructured":"Milner R (1980) A calculus of communicating systems, lecture notes in computer science, vol 92. Springer","DOI":"10.1007\/3-540-10235-3"},{"key":"1142_CR33","unstructured":"Milner R (1999) Communicating and mobile systems - the Pi-calculus. Cambridge University Press"},{"key":"1142_CR34","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/j.entcs.2004.10.029","volume":"142","author":"S Nanz","year":"2006","unstructured":"Nanz S, Hankin C (2006) Formal security analysis for ad-hoc networks. Electr Notes Theor Comput Sci 142:195\u2013213","journal-title":"Electr Notes Theor Comput Sci"},{"key":"1142_CR35","doi-asserted-by":"crossref","unstructured":"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\u2013204","DOI":"10.1007\/978-3-642-35861-6_12"},{"issue":"1-3","key":"1142_CR36","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn PW (2007) Resources, concurrency, and local reasoning. Theor Comput Sci 375(1-3):271\u2013307","journal-title":"Theor Comput Sci"},{"key":"1142_CR37","doi-asserted-by":"crossref","unstructured":"Perkins CE (1999) Belding-Royer EM Ad-hoc on-demand distance vector routing. In: 2nd Workshop on mobile computing systems and applications (WMCSA \u201999), February 25-26, 1999. New Orleans, LA, USA, pp 90-100","DOI":"10.1109\/MCSA.1999.749281"},{"key":"1142_CR38","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.jlap.2004.03.009","volume":"60-61","author":"GD Plotkin","year":"2004","unstructured":"Plotkin GD (2004) A structural approach to operational semantics. J Log Algebr Program 60-61:17\u2013139","journal-title":"J Log Algebr Program"},{"issue":"2-3","key":"1142_CR39","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/0167-6423(95)00017-8","volume":"25","author":"KVS Prasad","year":"1995","unstructured":"Prasad KVS (1995) A calculus of broadcasting systems. Sci Comput Program 25(2-3):285\u2013327","journal-title":"Sci Comput Program"},{"key":"1142_CR40","doi-asserted-by":"crossref","unstructured":"Rappaport TS (1996) Wireless communications - principles and practice. Prentice Hall","DOI":"10.1007\/978-1-4615-5491-2"},{"issue":"2","key":"1142_CR41","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1145\/1089733.1089736","volume":"37","author":"P Santi","year":"2005","unstructured":"Santi P (2005) Topology control in wireless ad hoc and sensor networks. ACM Comput Surv 37(2):164\u2013194","journal-title":"ACM Comput Surv"},{"key":"1142_CR42","doi-asserted-by":"crossref","unstructured":"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\u2013100","DOI":"10.1007\/978-3-642-15240-5_7"},{"key":"1142_CR43","doi-asserted-by":"crossref","unstructured":"Stoy JE (1979) Foundations of denotational semantics. In: Abstract software specifications, 1979 Copenhagen Winter School, January 22 - February 2, 1979, Proceedings, pp 43\u201399","DOI":"10.1007\/3-540-10007-5_35"},{"key":"1142_CR44","doi-asserted-by":"crossref","unstructured":"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\u2013231","DOI":"10.1109\/HASE.2015.40"},{"key":"1142_CR45","doi-asserted-by":"crossref","unstructured":"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\u2013227","DOI":"10.1109\/HASE.2016.29"},{"key":"1142_CR46","doi-asserted-by":"crossref","unstructured":"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\u201350","DOI":"10.1109\/COMPSAC.2017.32"}],"container-title":["Mobile Networks and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11036-018-1142-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-018-1142-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-018-1142-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,21]],"date-time":"2025-10-21T14:08:39Z","timestamp":1761055719000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11036-018-1142-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,29]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2,15]]}},"alternative-id":["1142"],"URL":"https:\/\/doi.org\/10.1007\/s11036-018-1142-8","relation":{},"ISSN":["1383-469X","1572-8153"],"issn-type":[{"value":"1383-469X","type":"print"},{"value":"1572-8153","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,9,29]]},"assertion":[{"value":"29 September 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}