Declarative Approach to Model Checking for Context-Aware Applications

  • Ammar AlsaigEmail author
  • Vangalur Alagar
  • Nematollaah Shiri
Conference paper
Part of the Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering book series (LNICST, volume 298)


Systems need to be formally verified to ensure that their claimed properties hold at all times of system operation. Deterministic Finite State Machines (FSM) are widely used as model checkers to verify system properties. However, for context-aware systems that have regular inputs and contextual inputs, FSM models become more complex and less intuitive, and do not precisely represent the system behavior. In this paper we use simple examples to introduce the declarative reasoning framework Contelog , a theoretically and practically well grounded work in progress, as a complementary approach that can be used to represent, reason, verify data-centric and contextual properties of context-aware systems.


Formal verification Context-aware modeling Model checking Context-based knowledge base systems 


  1. 1.
    Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases: the Logical Level. Addison-Wesley, Boston (1995)Google Scholar
  2. 2.
    Alsaig, A.: Book of examples: a prototype environment for reasoning with contexts (2017).
  3. 3.
    Alsaig, A., Alagar, V., Shiri, N.: Formal context representation and calculus for context-aware computing. In: Cong Vinh, P., Alagar, V. (eds.) ICCASA/ICTCC -2018. LNICST, vol. 266, pp. 3–13. Springer, Cham (2019). Scholar
  4. 4.
    Bresolin, D., El-Fakih, K., Villa, T., Yevtushenko, N.: Deterministic timed finite state machines: equivalence checking and expressive power. arXiv preprint arXiv:1408.5967 (2014)
  5. 5.
    Brézillon, P.: Context in problem solving: a survey. Knowl. Eng. Rev. 14(1), 47–80 (1999)CrossRefGoogle Scholar
  6. 6.
    Buchanan, B.G., Shortliffe, E.H., et al.: Rule-Based Expert Systems, vol. 3. Addison Wesley, Reading (1984)Google Scholar
  7. 7.
    Carminati, B., Ferrari, E., Perego, A.: Rule-based access control for social networks. In: Meersman, R., Tari, Z., Herrero, P. (eds.) OTM 2006. LNCS, vol. 4278, pp. 1734–1744. Springer, Heidelberg (2006). Scholar
  8. 8.
    Clancey, W.J.: The epistemology of a rule-based expert system–a framework for explanation. Artif. Intell. 20(3), 215–251 (1983)CrossRefGoogle Scholar
  9. 9.
    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer, Heidelberg (2018)CrossRefGoogle Scholar
  10. 10.
    Lamperti, G., Zanella, M.: Rule-Based Diagnosis, pp. 193–233. Springer, Dordrecht (2003)zbMATHGoogle Scholar
  11. 11.
    Le, H.A.: Formal modeling and verification of context-aware systems using event-b. EAI Endorsed Trans. Context-Aware Syst. Appl. 1, e4 (2014). Scholar
  12. 12.
    Liu, Y., Xu, C., Cheung, S.: Afchecker: effective model checking for context-aware adaptive applications. J. Syst. Soft. 86(3), 854–867 (2013)CrossRefGoogle Scholar
  13. 13.
    Schmidtke, H.R., Woo, W.: Towards ontology-based formal verification methods for context aware systems. In: Tokuda, H., Beigl, M., Friday, A., Brush, A.J.B., Tobe, Y. (eds.) Pervasive 2009. LNCS, vol. 5538, pp. 309–326. Springer, Heidelberg (2009). Scholar
  14. 14.
    Skelin, M., Wognsen, E.R., Olesen, M.C., Hansen, R.R., Larsen, K.G.: Model checking of finite-state machine-based scenario-aware dataflow using timed automata. In: 10th IEEE International Symposium on Industrial Embedded Systems (SIES), pp. 1–10. IEEE (2015)Google Scholar
  15. 15.
    Strang, T., Linnhoff-Popien, C.: A context modeling survey. In: Workshop Proceedings (2004)Google Scholar
  16. 16.
    Wagner, F., Schmuki, R., Wagner, T., Wolstenholme, P.: Modeling Software with Finite State Machines: A Practical Approach. Auerbach Publications (2006)Google Scholar

Copyright information

© ICST Institute for Computer Sciences, Social Informatics and Telecommunications Engineering 2019

Authors and Affiliations

  • Ammar Alsaig
    • 1
    Email author
  • Vangalur Alagar
    • 1
  • Nematollaah Shiri
    • 1
  1. 1.Concordia UniversityMontrealCanada

Personalised recommendations