Assuring Intelligent Ambient Assisted Living Solutions by Statistical Model Checking

  • Ashalatha KunnappillyEmail author
  • Raluca Marinescu
  • Cristina Seceleanu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11245)


A modern way of enhancing elderly people’s quality of life is by employing various Ambient Assisted Living solutions that facilitate an independent and safe living for their users. This is achieved by integrating computerized functions such as health and home monitoring, fall detection, reminders, etc. Such systems are safety critical, therefore ensuring at design time that they operate correctly, but also in a timely and robust manner is important. Most of the solutions are not analyzed formally at design time, especially if such Ambient Assisted Living functions are integrated within the same design. To address this concern, we propose a framework that relies on an abstract component-based description of the system’s architecture in the Architecture Analysis and Design Language. To ensure scalability of analysis, we transform the AADL models into a network of stochastic timed automata amenable to statistical analysis of various quality-of-service attributes. The architecture that we analyze is developed as part of the project CAMI, co-financed by the European Commission, and consists of a variety of health and home sensors, a data collector, local and cloud processing, as well as an artificial-intelligence-based decision support system. Our contribution paves the way towards achieving design-time assured integrated Ambient Assisted Living solutions, which in turn could reduce verification effort at later stages.



This work has been supported by the joint EU/Vinnova project grant CAMI, AAL-2014-1-087, which is gratefully acknowledged.


  1. 1.
    OSATE-Open Source AADL Test Environment. Accessed 15 May 2018
  2. 2.
    Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)MathSciNetzbMATHCrossRefGoogle Scholar
  3. 3.
    Augusto, J.C., Nugent, C.D.: The use of temporal reasoning and management of complex events in smart homes. In: Proceedings of the 16th European Conference on Artificial Intelligence, pp. 778–782. IOS Press (2004)Google Scholar
  4. 4.
    Bao, Y., Chen, M., Zhu, Q., Wei, T., Mallet, F., Zhou, T.: Quantitative performance evaluation of uncertainty-aware hybrid AADL designs using statistical model checking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 36(12), 1989–2002 (2017)CrossRefGoogle Scholar
  5. 5.
    Besnard, L., et al.: Formal semantics of behavior specifications in the architecture analysis and design language standard. In: Nakajima, S., Talpin, J.-P., Toyoshima, M., Yu, H. (eds.) Cyber-Physical System Design from an Architecture Analysis Viewpoint, pp. 53–79. Springer, Singapore (2017). Scholar
  6. 6.
    Bruintjes, H., Katoen, J.P., Lesens, D.: A statistical approach for timed reachability in AADL models. In: 45th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 81–88. IEEE (2015)Google Scholar
  7. 7.
    Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of WMTL. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 260–275. Springer, Heidelberg (2013). Scholar
  8. 8.
    David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397–415 (2015)CrossRefGoogle Scholar
  9. 9.
    Delange, J., Feiler, P.: Architecture fault modeling with the AADL error-model annex. In: 2014 40th EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA), pp. 361–368. IEEE (2014)Google Scholar
  10. 10.
    Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language. Addison-Wesley, Boston (2012)Google Scholar
  11. 11.
    Feiler, P.H., Lewis, B., Vestal, S., Colbert, E.: An overview of the SAE architecture analysis & design language (AADL) standard: a basis for model-based architecture-driven embedded systems engineering. In: Dissaux, P., Filali-Amine, M., Michel, P., Vernadat, F. (eds.) IFIP WCC TC2 2004. IFIP The International Federation for Information Processing, vol. 176. Springer, Boston (2005). Scholar
  12. 12.
    Frana, R., Bodeveix, J.P., Filali, M., Rolland, J.F.: The AADL behaviour annex-experiments and roadmap. In: 2007 12th IEEE International Conference on Engineering Complex Computer Systems, pp. 377–382. IEEE (2007)Google Scholar
  13. 13.
    Hamdane, M.E., Chaoui, A., Strecker, M.: From AADL to timed automaton-a verification approach. Int. J. Softw. Eng. Appl. 7(4), 115–126 (2013)Google Scholar
  14. 14.
    Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006). Scholar
  15. 15.
    Johnsen, A., Lundqvist, K., Pettersson, P., Jaradat, O.: Automated verification of AADL-specifications using UPPAAL. In: 2012 IEEE 14th International Symposium on High-Assurance Systems Engineering (HASE), pp. 130–138. IEEE (2012)Google Scholar
  16. 16.
    Kunnappilly, A., Marinescu, R., Seceleanu, C.: A Statistical Analysis Framework for Ambient Assisted Living Solutions. Technical report.
  17. 17.
    Kunnappilly, A., Seceleanu, C., Lindén, M.: Do we need an integrated framework for ambient assisted living? In: García, C.R., Caballero-Gil, P., Burmester, M., Quesada-Arencibia, A. (eds.) UCAmI/IWAAL/AmIHEALTH -2016, Part II. LNCS, vol. 10070, pp. 52–63. Springer, Cham (2016). Scholar
  18. 18.
    Kunnappilly, A., Sorici, A., Awada, I.A., Mocanu, I., Seceleanu, C., Florea, A.M.: A novel integrated architecture for ambient assisted living systems. In: 2017 IEEE 41st Annual Computer Software and Applications Conference (COMPSAC), vol. 1, pp. 465–472. IEEE (2017)Google Scholar
  19. 19.
    Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). Scholar
  20. 20.
    Li, R., Lu, B., McDonald-Maier, K.D.: Cognitive assisted living ambient system: a survey. Digit. Commun. Netw. 1(4), 229–252 (2015)CrossRefGoogle Scholar
  21. 21.
    Liu, Y., Gui, L., Liu, Y.: MDP-based reliability analysis of an ambient assisted living system. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 688–702. Springer, Cham (2014). Scholar
  22. 22.
    Magherini, T., Fantechi, A., Nugent, C.D., Vicario, E.: Using temporal logic and model checking in automated recognition of human activities for ambient-assisted living. IEEE Trans. Hum. Mach. Syst. 43(6), 509–521 (2013)CrossRefGoogle Scholar
  23. 23.
    Medjahed, H., Istrate, D., Boudy, J., Dorizzi, B.: Human activities of daily living recognition using fuzzy logic for elderly home monitoring. In: 2009 IEEE International Conference on Fuzzy Systems, FUZZ-IEEE 2009, pp. 2001–2006. IEEE (2009)Google Scholar
  24. 24.
    Parente, G., Nugent, C.D., Hong, X., Donnelly, M.P., Chen, L., Vicario, E.: Formal modeling techniques for ambient assisted living. Ageing Int. 36(2), 192–216 (2011)CrossRefGoogle Scholar
  25. 25.
    Rashidi, P., Mihailidis, A.: A survey on ambient-assisted living tools for older adults. IEEE J. Biomed. Health Inform. 17(3), 579–590 (2013)CrossRefGoogle Scholar
  26. 26.
    Rodrigues, G.N., Alves, V., Silveira, R., Laranjeira, L.A.: Dependability analysis in the ambient assisted living domain: an exploratory case study. J. Syst. Softw. 85(1), 112–131 (2012)CrossRefGoogle Scholar
  27. 27.
    Zhou, F., Jiao, J.R., Chen, S., Zhang, D.: A case-driven ambient intelligence system for elderly in-home assistance applications. IEEE Trans. Syst. Man Cybern. Part C (Appl. Rev.) 41(2), 179–189 (2011)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Ashalatha Kunnappilly
    • 1
    Email author
  • Raluca Marinescu
    • 1
  • Cristina Seceleanu
    • 1
  1. 1.Mälardalen UniversityVästeråsSweden

Personalised recommendations