Context-Aware Systems and Applications, and Nature of Computation and Communication. 8th EAI International Conference, ICCASA 2019, and 5th EAI International Conference, ICTCC 2019, My Tho City, Vietnam, November 28-29, 2019, Proceedings

Research Article

Declarative Approach to Model Checking for Context-Aware Applications

Download
241 downloads
  • @INPROCEEDINGS{10.1007/978-3-030-34365-1_1,
        author={Ammar Alsaig and Vangalur Alagar and Nematollaah Shiri},
        title={Declarative Approach to Model Checking for Context-Aware Applications},
        proceedings={Context-Aware Systems and Applications, and Nature of Computation and Communication. 8th EAI International Conference, ICCASA 2019, and 5th EAI International Conference, ICTCC 2019, My Tho City, Vietnam, November 28-29, 2019, Proceedings},
        proceedings_a={ICCASA \& ICTCC},
        year={2019},
        month={12},
        keywords={Formal verification Context-aware modeling Model checking Context-based knowledge base systems},
        doi={10.1007/978-3-030-34365-1_1}
    }
    
  • Ammar Alsaig
    Vangalur Alagar
    Nematollaah Shiri
    Year: 2019
    Declarative Approach to Model Checking for Context-Aware Applications
    ICCASA & ICTCC
    Springer
    DOI: 10.1007/978-3-030-34365-1_1
Ammar Alsaig1,*, Vangalur Alagar1,*, Nematollaah Shiri1,*
  • 1: Concordia University
*Contact email: A_alsaig@encs.concordia.ca, alagar@encs.concordia.ca, shiri@encs.concordia.ca

Abstract

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 , 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.