Abstract
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 formal verification, 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, Scatterbox. 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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
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
Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2): 183–235
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
Bakhouya M, Campbell R, Coronato A, de Pietro G, Ranganathan A (2012) Introduction to special section on formal methods in pervasive computing. ACM Trans Auton Adapt Syst 7(1): 6–169
Bozga M, Daws C, Maler O, Olivero A, Tripakis S, Yovine S (1998) Kronos: a model-checking tool for real-time systems. In: CAV ’98 Proceedings of the 10th international conference on computer aided verification. Springer, Berlin, pp 546–550
Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge
Bengtsson J, Larsen KG, Larsson F, Pettersson P, Yi W (1995) Uppaal—a tool suite for automatic verification of real–time systems. In: Proceedings of workshop on verification and control of hybrid systems III(1066). Lecture Notes in Computer Science, pp 232–243. Springer, Berlin
Boytsov A, Zaslavsky A (2013) Formal verification of context and situation models in pervasive computing. Pervasive Mob Comput 9(1): 98–117
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’99), pp 495–499
Coronato A, De Pietro G (2011) Formal specification and verification of ubiquitous and pervasive systems. ACM Trans Autonom Adap Syst 6(1):9
Chen H, Finin T, Joshi A (2003) An ontology for context-aware pervasive computing environments. Knowl Eng Rev 18(3): 197–207
Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge
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
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–191
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–305. Springer, Berlin
Dobson S, Sterritt R, Nixon P, Hinchey M (2010) Fulfilling the vision of autonomic computing. IEEE Comput 43(01): 35–41
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–86
Hansson H., Jonsson B (1994) A logic for reasoning about time and reliability. Formal Asp Comput 6: 102–111
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–444. Springer, Berlin
Holzmann GJ (2003) The spin model checker. Addison-Wesley, Reading
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–85
Konur S, Dixon C, Fisher M (2012) Analysing robot swarm behaviour via probabilistic model checking. Robot Auton Syst 60(2): 199–213
Katoen J-P, Khattri M, Zapreev IS (2005) A Markov Reward model checker. In: QEST. pp 243–244
Kwiatkowska MZ, Norman G, Parker D (2008) Using probabilistic model checking in systems biology. SIGMETRICS Perform Eval Rev 35(4): 14–21
Kwiatkowska M, Norman G, Parker D, Sproston J (2006) Performance analysis of probabilistic timed automata using digital clocks. Form Methods Syst Des 29(1): 33–78
Kwiatkowska M, Norman G, Segala R, Sproston J (2002) Automatic verification of real-time systems with discrete probability distributions. Theor Comput Sci 282(1): 101–150
Knox S, Shannon R, Coyle L, Clear A, Dobson S, Quigley A, Nixon P (2008) Scatterbox: context-aware message management. Rev Intell Artif 22(5): 549–568
Katoen J-P, Zapreev IS, Hahn EM, Hermanns H, Jansen DN (2011) The ins and outs of the probabilistic model checker MRMC. Perform Eval 68(2): 90–104
Liu Y, Zhang X, Dong JS, Liu Y, Sun J, Biswas J, Mokhtari M (2012) Formal analysis of pervasive computing systems. IEEE Int Conf Eng Complex Comput Syst 0:169–178
Prism Manual (2011) http://www.prismmodelchecker.org/manual
Ranganathan A, Campbell RH (2008) Provably correct pervasive computing environments. IEEE Int Conf Pervasive Comput Commun 0:160–169
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’05) pp 206–212. IEEE Computer Society Press
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
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–162
Sen K, Viswanathan M, Agha G (2005) On statistical model checking of stochastic systems. In: CAV. pp 266–280
Weis T, Becker C, Brändle 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
Want R, Pering T, Borriello G, Farkas KI (2002) Disappearing hardware. Pervasive Comput, IEEE 1(1): 36–47
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–22
Younes HLS (2005) Ymer: a statistical model checker. In: CAV. pp 429–433
Author information
Authors and Affiliations
Corresponding author
Additional information
Dong Jin Song
Rights and permissions
About this article
Cite this article
Konur, S., Fisher, M., Dobson, S. et al. Formal verification of a pervasive messaging system. Form Asp Comp 26, 677–694 (2014). https://doi.org/10.1007/s00165-013-0277-4
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-013-0277-4