Keynote by Carlo Ghezzi
Adaptive software needs continuous verification
Date: Tuesday September 14th Time: 9.15 - 10.15
Modern software applications are increasingly embedded in an open world that is constantly evolving, because of changes in the requirements, in the environment, and in usage profiles. These changes are difficult to predict and anticipate, and are out of control of the application. In many cases, changes cannot be handled off-line, but require the software to self-react by adapting its behavior dynamically, to continue to ensure the desired quality of service. The big challenge in front of us is how to achieve the necessary degrees of flexibility and dynamism required by software applications without compromising the needed dependability.
The talk focuses on quantitative probabilistic requirements. It discusses how the initial design of an application may proceed through a model-driven process towards an implementation that satisfies requirements. Design-time parameters characterizing the environment are intrinsically subject to uncertainty, both because predictions are intrinsically inaccurate and because the environment is likely to change. It is thus necessary to check at run time if these parameters change significantly and may eventually lead to requirements violations.
To do so, we need to extend verification to run time, by monitoring the environment, in order to get the real data that characterize it and affect the behavior of the application, and feeding the model (which continues to exist at run time) with new parameters, replacing the outdated values that were used at development time. The updated model can check whether the requirements are still met, or whether a reconfiguration is needed in the application in order to continue to satisfy the requirements.
The talk reports on some results of recent research, developed within the SMScom project, funded by the European Commission, Programme IDEAS-ERC, Project 227977 (http://www.erc-smscom.org/). The focus is on modelling, model update, and automatic reasoning on requirements. An initial attempt to support self-adapting reactions will also be outlined.