Modern software-intensive systems often interact with an environment whose behavior changes over time, often
unpredictably. The occurrence of changes may jeopardize their ability to meet the desired requirements. It is therefore desirable to
design software in a way that it can self-adapt to the occurrence of changes with limited, or even without, human intervention.
Self-adaptation can be achieved by bringing software models and model checking to run time, to support perpetual automatic
reasoning about changes. Once a change is detected, the system itself can predict if requirements violations may occur and enable
appropriate counter-actions. However, existing mainstream model checking techniques and tools were not conceived for run-time
usage; hence they hardly meet the constraints imposed by on-the-fly analysis in terms of execution time and memory usage. This
paper addresses this issue and focuses on perpetual satisfaction of non-functional requirements, such as reliability or energy
consumption. Its main contribution is the description of a mathematical framework for run-time efficient probabilistic model checking.
Our approach statically generates a set of verification conditions that can be efficiently evaluated at run time as soon as changes occur.
The proposed approach also supports sensitivity analysis, which enables reasoning about the effects of changes and can drive
effective adaptation strategies.