Incremental Verification of Inductive Invariants for the Run-Time Evolution of Self-Adaptive Software-Intensive Systems

The safe run-time evolution of complex software-intensive systems requires that the impact of changes can be predicted at run-time. In this paper we consider the specific case of self-adaptive software-intensive systems using an example for the coordination of autonomous vehicles. We show how incremental run-time checks can verify that changes in the rule set which governs the distributed rule-based self-adaptive behavior provides the required safety properties. We demonstrate how an existing verification technique for invariant checking is turned into an incremental one. We discuss the theoretical complexity of the incremental verification checks and also present some first evaluation results.