Adaptive Software Needs Continuous Verification
Carlo Ghezzi · 2010
Modern software applications increasingly live in an open world, characterized by continuous change in the environment in which they are situated and in the requirements they have to meet. Continuous changes occur autonomously and unpredictably, in a way that can hardly be predicted (and taken care of) by software engineers, as the application is designed. As a consequence, changes are out of control of the running application, which cannot handle them. On the other hand, there is an increasing demand for software solutions that can easily evolve and dynamically adapt their behavior to provide continuous service as changes occur. This is especially needed when systems must be perpetually running and cannot be changed off-line. Hereafter I focus on environment changes that may affect an application. This may include changes in the way people interact with the system or changes in the external components, which offer services upon which the currently developed application relies. Moreover, I will mostly focus on quantitatively stated requirements that express nonfunctional properties of an application, such as performance or reliability. Because of the uncertainty that characterizes open-world settings, requirements should be expressed in probabilistic terms. I will argue that models at run-time are needed to support continuous verification. Furthermore, I will discuss why continuous verification is needed to support an on-line update of the application's model, which-in turn-may support formal approaches to software evolution. I focus on system requirements that are stated in quantitative and probabilistic terms, such as reliability and performance requirements. I also focus on the use of Markov models, which may be used at design-time to verify satisfaction of the requirements, based on assumptions on the behavior of the environment. Assuming, for instance, that the whole system is modeled as a Discrete-Time Markov Chain, probabilities attached to transitions may be used to represent user profiles (e.g., the probability that a certain operation is invoked by the user). They may also represent failure rates of external services used by the application, or performance figures about their response time. Once the model is built at design-time, one can state properties that the system should satisfy and use the model to check if such properties are verified, for example through automated probabilistic model checking (e.g. By monitoring the environment at run-time, we collect data that correspond to the actual external behaviors that may affect the application. For example, we monitor user interactions as well as the real failure rates and response time of external components. The collected data may be analyzed by a machine learning process, which may produce updated estimates for the probabilities attached to the transitions of the DTMC model of the application. As the model is updated with current values of the parameters, it can be run to check if the desired properties of the application, which were proved to hold at development time, still hold at run-time. In case they do, no action is in general required. Instead, if a violation occurs, suitable recovery actions must be put in place. One may distinguish here between two cases that characterize a violation of the desired global properties. The violation may correspond to a predicted future failure of the running system or it may correspond to an actually experienced failure. The former case should trigger a preventive recovery procedure, whose success may assure that no failure will be experienced in practice. The latter case instead triggers a recovery procedure that tries to compensate the effect of the experienced failure. The view discussed here is currently being investigated in all its facets by the DeepSE Group at Politecnico di Milano. Moreover a prototype environment (called KAMI) is being developed to support both development-time modeling and analysis and run-time model evolution. In turn, run-time verification supports adaptation, both to prevent failures and to recover from them. Future work will consolidate the current approach and will focus on several unresolved issues, such as understanding and supporting run-time adaptation strategies (a preliminary approach is described in, and devising further approaches to run-time verification that may lead to time-efficient analysis at run-time without the need for using time-expensive model checkers. This-in turn-would enable reactions that may satisfy stringent time constraints.