A contract-based approach to adaptivity

Adaptive systems are systems capable of adapting their behaviour to changes in their environment. Creating such systems is not an easy task, however. Especially, creating such a system as one monolithic software component taking all eventualities and environments into account bears the risk of bad system design. To circumvent this risk, an adaptive system can be composed from partial solutions handling only a subset of all possible circumstances and environments. Then, the system can be changed through reconfigurations as the environment evolves. In this paper, we propose an approach for the verification of systems using reconfiguration as means of adaptation. For the specification of such systems and their components we introduce reMitl which is based on Metric Interval Temporal Logic Mitl and allows to express connectivity of components. Based on an example from the domain of pervasive computing, we show how a system undergoing reconfigurations can be verified to satisfy a global assume-guarantee contract expressed as a pair of reMitl formulas.