Abstract
This paper complements our previous work on formal modeling of resource-bounded context-aware systems, which handle inconsistent context information using defeasible reasoning, by focusing on automated analysis and verification. A case study demonstrates how model checking techniques can be used to formally analyze quantitative and qualitative properties of a context-aware system based on message passing among agents. The behavior (semantics) of the system is modeled by a term rewriting system and the desired properties are expressed as LTL formulas. The Maude LTL model checker is used to perform automated analysis of the system and verify non-conflicting context information guarantees it provides.
| Original language | English |
|---|---|
| Title of host publication | 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) |
| Place of Publication | Austin, TX, USA |
| Publisher | IEEE |
| Pages | 61-69 |
| Number of pages | 9 |
| ISBN (Electronic) | 978-1-5090-0237-5 |
| ISBN (Print) | 978-1-5090-0238-2 |
| DOIs | |
| Publication status | Published - 21 Sept 2015 |
| Externally published | Yes |
| Event | 13th ACM-IEEE International Conference on Formal Methods and Models for System Design - The University of Texas at Austin, Texas at Austin, United States Duration: 21 Sept 2015 → 23 Sept 2015 Conference number: 13 http://memocode.irisa.fr/2015/ |
Conference
| Conference | 13th ACM-IEEE International Conference on Formal Methods and Models for System Design |
|---|---|
| Abbreviated title | MEMOCODE'15 |
| Country/Territory | United States |
| City | Texas at Austin |
| Period | 21/09/15 → 23/09/15 |
| Internet address |
Keywords
- Formal modeling
- Model checking
- Context-aware systems
- Rule-based reasoning
- Defeasible reasoning
- Multi-agent systems