{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T09:01:14Z","timestamp":1762506074116,"version":"3.40.4"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>As ubiquitous computing becomes a reality, its applications are increasingly being used in business-critical, mission-critical and even in safety-critical, areas. Such systems must demonstrate an assured level of correctness. One approach to the exhaustive analysis of the behaviour of systems is<jats:italic>formal verification<\/jats:italic>, whereby each important requirement is logically assessed against all possible system behaviours. While formal verification is often used in safety analysis, it has rarely been used in the analysis of deployed pervasive applications. Without such formality it is difficult to establish that the system will exhibit the correct behaviours in response to its inputs and environment. In this paper, we show how model-checking techniques can be applied to analyse the probabilistic behaviour of pervasive systems. As a case study we apply this technique to an existing pervasive message-forwarding system,<jats:italic>Scatterbox<\/jats:italic>. Scatterbox incorporates many typical characteristics of pervasive systems, such as dependence on sensor reliability and dependence on context. We assess the dynamic temporal behaviour of the system, including the analysis of probabilistic elements, allowing us to verify formal requirements even in the presence of uncertainty in sensors. We also draw some tentative conclusions concerning the use of formal verification for pervasive computing in general.<\/jats:p>","DOI":"10.1007\/s00165-013-0277-4","type":"journal-article","created":{"date-parts":[[2013,3,27]],"date-time":"2013-03-27T15:37:05Z","timestamp":1364398625000},"page":"677-694","source":"Crossref","is-referenced-by-count":15,"title":["Formal verification of a pervasive messaging system"],"prefix":"10.1145","volume":"26","author":[{"given":"Savas","family":"Konur","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Dobson","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of St Andrews, St Andrews, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen","family":"Knox","sequence":"additional","affiliation":[{"name":"School of Computer Science and Informatics, UCD Dublin, Dublin, Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Arapinis M Calder M Denis L Fisher M Gray P Konur S Miller A Ritter E Ryan M Schewe S Unsworth C Yasmin R (2009) Towards the verification of pervasive systems. In: 3rd international workshop on formal methods for interactive systems (FMIS) Vol 22. Electronic Communications of the EASST"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_3_2","unstructured":"Birkedal L Bundgaard M Damgaard TC Debois S Elsborg E Glenstrup AJ Hildebr T Milner R Niss H (2006) Bigraphical programming languages for pervasive computing. In: International workshop on combining theory and systems building in pervasive computing"},{"issue":"1","key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1145\/2168260.2168266","article-title":"Introduction to special section on formal methods in pervasive computing","volume":"7","author":"Bakhouya M","year":"2012","journal-title":"ACM Trans Auton Adapt Syst"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bozga M Daws C Maler O Olivero A Tripakis S Yovine S (1998) Kronos: a model-checking tool for real-time systems. In: CAV \u201998 Proceedings of the 10th international conference on computer aided verification. Springer Berlin pp 546\u2013550","DOI":"10.1007\/BFb0028779"},{"volume-title":"Principles of model checking","year":"2008","author":"Baier C","key":"e_1_2_1_2_6_2"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bengtsson J Larsen KG Larsson F Pettersson P Yi W (1995) Uppaal\u2014a tool suite for automatic verification of real\u2013time systems. In: Proceedings of workshop on verification and control of hybrid systems III(1066). Lecture Notes in Computer Science pp 232\u2013243. Springer Berlin","DOI":"10.1007\/BFb0020949"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2012.03.001"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Cimatti A Clarke E Giunchiglia F Roveri M (1999) Nusmv: a new symbolic model verifier. In: Proceedings of international conference on computer-aided verification (CAV\u201999) pp 495\u2013499","DOI":"10.1007\/3-540-48683-6_44"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/1921641.1921650"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888904000025"},{"key":"e_1_2_1_2_12_2","unstructured":"Clarke EM Grumberg O Peled D (1999) Model checking. MIT Press Cambridge"},{"key":"e_1_2_1_2_13_2","unstructured":"Calder M Gray P Unsworth C (2009) Tightly coupled verification of pervasive systems. In: 3rd international workshop on formal methods for interactive systems (FMIS) Vol 22. Electronic Communications of the EASST"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Cubo J Sama M Raimondi F Rosenblum D (2009) A model to design and verify context-aware adaptive service composition. In Proceedings of the IEEE International Conference on Services Computing (SCC). pp 184\u2013191","DOI":"10.1109\/SCC.2009.61"},{"key":"e_1_2_1_2_15_2","unstructured":"Dobson SA Nixon P (2005) More principled design of pervasive computing systems. In: Bastide R Palanque PA Roth J (eds) Proceedings of the joint working conferences on engineering human computer interaction and interactive systems (EHCI-DSVIS) vol 3425 of LNCS pp 292\u2013305. Springer Berlin"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2010.14"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Henricksen K Indulska J (2004) A software engineering framework for context-aware pervasive computing. In: Proceedings 2nd IEEE conference on pervasive computing and communications. pp 77\u201386","DOI":"10.1109\/PERCOM.2004.1276847"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Hinton A Kwiatkowska M Norman G Parker D (2006) PRISM: a tool for automatic verification of probabilistic systems. In Proceedings of the TACAS vol 3920 of LNCS pp 441\u2013444. Springer Berlin","DOI":"10.1007\/11691372_29"},{"key":"e_1_2_1_2_20_2","unstructured":"Holzmann GJ (2003) The spin model checker. Addison-Wesley Reading"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Jansen DN Katoen J-P Oldenkamp M Stoelinga M Zapreev IS (2007) How fast and fat is your probabilistic model checker? An experimental performance comparison. In: Haifa verification conference. pp 69\u201385","DOI":"10.1007\/978-3-540-77966-7_9"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2011.10.005"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Katoen J-P Khattri M Zapreev IS (2005) A Markov Reward model checker. In: QEST. pp 243\u2013244","DOI":"10.1109\/QEST.2005.2"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/1364644.1364651"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0005-2"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00046-9"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.3166\/ria.22.549-568"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2010.04.001"},{"key":"e_1_2_1_2_29_2","first-page":"169","article-title":"Formal analysis of pervasive computing systems","volume":"0","author":"Liu Y","year":"2012","journal-title":"IEEE Int Conf Eng Complex Comput Syst"},{"key":"e_1_2_1_2_30_2","unstructured":"Prism Manual (2011) http:\/\/www.prismmodelchecker.org\/manual"},{"key":"e_1_2_1_2_31_2","first-page":"160","article-title":"Provably correct pervasive computing environments","volume":"0","author":"Ranganathan A","year":"2008","journal-title":"IEEE Int Conf Pervasive Comput Commun"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Sheng QZ Benatallah B (2005) Contextuml: a UML-based modeling language for model-driven development of context-aware web services. In: Proceedings of the International Conference on Mobile Business (ICMB\u201905) pp 206\u2013212. IEEE Computer Society Press","DOI":"10.1109\/ICMB.2005.33"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Simons C (2007) CMP: a UML context modeling profile for mobile distributed systems. In: Proceedings of the 40th Hawaii International Conference on System Sciences p 289. IEEE Computer Society Press","DOI":"10.1109\/HICSS.2007.125"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Sun J Liu Y Song S Dong JS Li X (2011) PRTS: an approach for model checking probabilistic real-time hierarchical systems. In ICFEM. pp 147\u2013162","DOI":"10.1007\/978-3-642-24559-6_12"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Sen K Viswanathan M Agha G (2005) On statistical model checking of stochastic systems. In: CAV. pp 266\u2013280","DOI":"10.1007\/11513988_26"},{"key":"e_1_2_1_2_36_2","unstructured":"Weis T Becker C Br\u00e4ndle E (2006) Towards a programming paradigm for pervasive applications based on the ambient calculus. In: International workshop on combining theory and systems building in pervasive computing"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/MPRV.2002.993143"},{"key":"e_1_2_1_2_38_2","unstructured":"Wang XH Zhang DQ Gu T Pung HK (2004) Ontology-based context modeling and reasoning using OWL. In: Context modeling and reasoning workshop at PerCom 04. pp 18\u201322"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Younes HLS (2005) Ymer: a statistical model checker. In: CAV. pp 429\u2013433","DOI":"10.1007\/11513988_43"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-013-0277-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-013-0277-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-013-0277-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T02:20:06Z","timestamp":1745979606000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-013-0277-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":39,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1007\/s00165-013-0277-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-013-0277-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2014,7]]}}}