Abstract
Smart systems equipped with emerging pervasive computing technologies enable people with limitations to live in their homes independently. However, lack of guarantees for correctness prevent such system to be widely used. Analysing the system with regard to correctness requirements is a challenging task due to the complexity of the system and its various unpredictable faults. In this work, we propose to use formal methods to analyse pervasive computing (PvC) systems. Firstly, a formal modelling framework is proposed to cover the main characteristics of such systems (e.g., context-awareness, concurrent communications, layered architectures). Secondly, we identify the safety requirements (e.g., free of deadlocks and conflicts) and specify them as safety and liveness properties. Furthermore, based on the modelling framework, we propose an approach of verifying reasoning rules which are used in the middleware for perceiving the environment and making adaptation decisions. Finally, we demonstrate our ideas using a case study of a smart healthcare system. Experimental results show the usefulness of our approach in exploring system behaviours and revealing system design flaws such as information inconsistency and conflicting reminder services.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Located at 9 Upper Changi Road North, Singapore, 507706. Tel: +65-65465678.
- 2.
Drools Expert: http://www.jboss.org/drools/drools-expert.html
- 3.
St- States, OOM- Out of Memory.
References
Weiser, M.: The computer for the 21st century. Sci. Am. 265(3), 66–75 (1991)
Estrin, D., Culler, D., Pister, K., Sukhatme, G.: Connecting the physical world with pervasive networks. IEEE Pervasive Comput. 1(1), 59–69 (2002)
Nehmer, J., Becker, M., Karshmer, A., Lamm, R.: Living assistance systems: an ambient intelligence approach. In: Proceedings of the 28th International Conference on Software Engineering, ICSE ’06, pp. 43–50 (2006)
Saha, D., Mukherjee, A.: Pervasive computing: a paradigm for the 21st century. Computer 36, 25–31 (2003)
Edwards, W.K., Grinter, R.E.: At home with ubiquitous computing: seven challenges. In: Abowd, G.D., Brumitt, B., Shafer, S. (eds.) Ubicomp 2001. LNCS, vol. 2201, pp. 256–272. Springer, Heidelberg (2001)
Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating specification and programs for system modeling and verification. In: TASE, pp. 127–135 (2009)
Dong, J.S., Feng, Y., Sun, J., Sun, J.: Context awareness systems design and reasoning. In: ISoLA, pp. 335–340 (2006)
Coronato, A., Pietro, G.D.: Formal specification of wireless and pervasive healthcare applications. ACM Trans. Embed. Comput. Syst. 10, 12:1–12:18 (2010)
Mahony, B., Dong, J.S.: Blending object-Z and timed CSP: an introduction to TCOZ. In: ICSE ’99, pp. 95–104 (1998)
Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)
Arapinis, M., Calder, M., Denis, L., Fisher, M., Gray, P.D., Konur, S., Miller, A., Ritter, E., Ryan, M., Schewe, S., Unsworth, C., Yasmin, R.: Towards the verification of pervasive systems. ECEASST 22, 1–15 (2009)
Clarke Jr, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Ligeza, A., Nalepa, G.J.: Rules verification and validation. In: Giurca, A., Gasevic, K.T.D. (eds.) Handbook of Research on Emerging Rule-Based Languages and Technologies: Open Solutions and Approaches, pp. 273–301. IGI Global, Hershey (2009)
Preece, A.D., Shinghal, R., Batarekh, A.: Principles and practice in verifying rule-based systems. Knowl. Eng. Rev. 7(02), 115–141 (1992)
Biswas, J., Mokhtari, M., Dong, J.S., Yap, P.: Mild dementia care at home – integrating activity monitoring, user interface plasticity and scenario verification. In: Lee, Y., Bien, Z.Z., Mokhtari, M., Kim, J.T., Park, M., Kim, J., Lee, H., Khalil, I. (eds.) ICOST 2010. LNCS, vol. 6159, pp. 160–170. Springer, Heidelberg (2010)
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)
Liu, Y., Zhang, X., Liu, Y., Sun, J., Dong, J.S., Biswas, J., Mokhtari, M.: Technical report for formal analysis pervasive computing systems. http://www.comp.nus.edu.sg/~yanliu/techreport.pdf
Olveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in real-time maude. Theor. Comput. Sci. 410, 254–280 (2009)
Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., Andre, E.: Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans. Software Eng. Methodol. (TOSEM) 22(1), 3:1–3:29 (2013)
Alur, R.: Timed automata. Theor. Comput. Sci. 126, 183–235 (1999)
Sun, J., Song, S., Liu, Y.: Model checking hierarchical probabilistic systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 388–403. Springer, Heidelberg (2010)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Marrero, W., Clarke, E., Jha, S.: Model checking for security protocols. Technical report. Carnegie Mellon University (1997)
Du, K., Zhang, D., Zhou, X., Hariz, M.: Handling conflicts of context-aware reminding system in sensorised home. Cluster Comput. 14, 81–89 (2011)
Antoniou, G.: Rule-based activity recognition in ambient intelligence. In: Bassiliades, N., Governatori, G., Paschke, A. (eds.) RuleML 2011 - Europe. LNCS, vol. 6826, pp. 1–1. Springer, Heidelberg (2011)
Storf, H., Becker, M., Riedl, M.: Rule-based activity recognition framework: challenges, technique and learning. In: PervasiveHealth, pp. 1–7 (2009)
Lee, V.Y., Liu, Y., Zhang, X., Phua, C., Sim, K., Zhu, J., Biswas, J., Dong, J.S., Mokhtari, M.: ACARP: auto correct activity recognition rules using process analysis toolkit (PAT). In: Donnelly, M., Paggetti, C., Nugent, C., Mokhtari, M. (eds.) ICOST 2012. LNCS, vol. 7251, pp. 182–189. Springer, Heidelberg (2012)
Sama, M., Elbaum, S., Raimondi, F., Rosenblum, D.S., Wang, Z.: Context-aware adaptive applications: fault patterns and their automated identification. IEEE Trans. Softw. Eng. 36, 644–661 (2010)
Acknowledgment
The authors would like to thank Lee Vwen Yen Alwyn, Clifton Phua, Zhu Jiaqi and Kelvin Sim from Institute for Infocomm Research in Singapore for the kindness contributions and valuable feedback to this work. We also want thanks the anonymous reviews for their valuable suggestions in improving the manuscript.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Liu, Y. et al. (2014). Towards Formal Modelling and Verification of Pervasive Computing Systems. In: Kowalczyk, R., Nguyen, N. (eds) Transactions on Computational Collective Intelligence XVI. Lecture Notes in Computer Science(), vol 8780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44871-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-662-44871-7_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44870-0
Online ISBN: 978-3-662-44871-7
eBook Packages: Computer ScienceComputer Science (R0)