Declarative Approach to Model Checking for Context-Aware Applications

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.