Run-time Validation of Behavioral Adaptations

Context-oriented programming enables the composition of behavioral adaptations into a running software system.
Behavioral adaptations provide the most appropriate behavior of a system when their contexts are activated or deactivated, according to the situations at hand in the system's execution environment.
Behavioral adaptations can be defined by third-party vendors or even be acquired at run time.
As the systems grows in complexity it becomes increasingly difficult to reason about every possible runtime adaptation.
Therefore, behavioral adaptations that lead to erroneous states or compromise the system's security might be difficult to detect statically.
To prevent such undesired behavioral adaptations from happening, we introduce a run-time correctness verification approach. Our approach uses a symbolic execution engine to reason about the reachable states of the system, whenever contexts are activated or deactivated. Context activation and deactivation requests are allowed depending on the presence of erroneous states within reachable states. Our approach is a step forward to ensure the run-time correctness of software systems that adapt their behavior dynamically.