A formal approach to modelling and verifying resource-bounded context-aware agents

Rakib, Abdur; Faruqui, Rokan Uddin

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. © 2013 ICST Institute for Computer Science, Social Informatics and Telecommunications Engineering.

Citation

Rakib, A., & Faruqui, R. U. (2013). A formal approach to modelling and verifying resource-bounded context-aware agents. Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, 109 LNICST, 86-96. https://doi.org/10.1007/978-3-642-36642-0_9

• Journal Article Type: Conference Paper
• Publication Date: Mar 14, 2013
• Deposit Date: Jun 16, 2017
• Journal: Lecture Notes of the Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering
• Print ISSN: 1867-8211
• Publisher: Springer Verlag (Germany)
• Peer Reviewed: Peer Reviewed
• Volume: 109 LNICST
• Pages: 86-96
• Book Title: Context-Aware Systems and Applications
• ISBN: 9783642366413
• DOI: https://doi.org/10.1007/978-3-642-36642-0_9
• Keywords: pervasive computing, context-awareness, multi-agent systems, ontology, model checking
• Public URL: https://uwe-repository.worktribe.com/output/939949
• Publisher URL: http://dx.doi.org/10.1007/978-3-642-36642-0_9
• Related Public URLs: https://link.springer.com/chapter/10.1007/978-3-642-36642-0_9