An Algebraic Framework for the Verification of Context-Aware Adaptive Systems

作者：Ksystra Katerina^*; Stefaneas Petros; Frangos Panayiotis

来源：International Journal of Software Engineering and Knowledge Engineering, 2015, 25(7): 1105-1128.

DOI：10.1142/S0218194015500199

• Context-aware adaptive systems
• algebraic specification
• OTS/CafeOBJ method
• formal methods
• specification
• verification

Context-aware and self adaptive systems have become very popular during the last decade. As these technologies are increasingly used in the development of critical applications, their behavior should be extensively analyzed. While formal methods provide a wide range of techniques for reasoning about software systems, addressing formally the requirements of context-aware adaptive systems in a consistent way remains a challenge. To this end, in this paper we present an algebraic framework for their formal specification using Observational Transition Systems (OTSs) specified in the CafeOBJ algebraic specification language. This approach permits the verification of the design of such systems, and can be an effective approach to obtaining verified context-aware software. We apply the proposed framework to the modeling of a context-aware adaptive traffic monitoring system and use theorem proving techniques to prove safety properties for that system.

• 出版日期2015-9