AC-Contract: Run-Time Verification of Context-Aware Applications

Modern software systems are increasingly complex and are controlling critical activities in many different domains. The traditional assumption that these systems will work in a controlled context is slightly vanishing. Therefore, it emerges the need of methodologies able to determine under what conditions desired goals will be achieved and behavioural strategies will be preserved despite (often unavoidable) adaptations. In this paper we use the cognitive psychology concept of schema to identify the set of properties that an adaptable system has to maintain when adapting to changed context. The methodology we propose, called AC-contract (Adaptable Code-contract), starts from high-level requirements and identifies properties that should hold locally on single parts of the system. Local properties are represented as contracts directly on the programming language. Specifically, AC-contract is able to embed logical propositions in the source code as annotations, moreover, it enables verification of adaptable code by exploiting a preprocessor that executes the annotations. The methodology is applied to a mobile application supporting travellers during their journey.