Context-Aware Systems and Applications. First International Conference, ICCASA 2012, Ho Chi Minh City, Vietnam, November 26-27, 2012, Revised Selected Papers

Research Article

A Formal Approach to Modelling and Verifying Resource-Bounded Context-Aware Agents

Download15 downloads
  • @INPROCEEDINGS{10.1007/978-3-642-36642-0_9,
        author={Abdur Rakib and Rokan Faruqui},
        title={A Formal Approach to Modelling and Verifying Resource-Bounded Context-Aware Agents},
        proceedings={Context-Aware Systems and Applications. First International Conference, ICCASA 2012, Ho Chi Minh City, Vietnam, November 26-27, 2012, Revised Selected Papers},
        proceedings_a={ICCASA},
        year={2013},
        month={2},
        keywords={Pervasive computing Context-awareness Multi-agent systems Ontology Model checking},
        doi={10.1007/978-3-642-36642-0_9}
    }
    
  • Abdur Rakib
    Rokan Faruqui
    Year: 2013
    A Formal Approach to Modelling and Verifying Resource-Bounded Context-Aware Agents
    ICCASA
    Springer
    DOI: 10.1007/978-3-642-36642-0_9
Abdur Rakib1,*, Rokan Faruqui2,*
  • 1: University of Nottingham
  • 2: University of Chittagong
*Contact email: Abdur.Rakib@nottingham.edu.my, rufaruqui@cu.ac.bd

Abstract

There has been a move of context-aware systems into safety-critical domains including healthcare, emergency scenarios, and disaster recovery. These systems are often distributed and deployed on resource-bounded devices. Therefore, developing formal techniques for modelling and designing context-aware systems, verifying requirements and ensuring functional correctness are major challenges. We present a framework for the formal representation and verification of resource-bounded context-aware systems. We give ontological representation of contexts, translate ontologies to a set of Horn clause rules, based on these rules we build multi-agent context-aware systems and encode them into Maude specification, we then verify interesting properties of such systems using the Maude LTL model checker.