Research Article
A Formal Approach to Modelling and Verifying Resource-Bounded Context-Aware Agents
@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
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.
