Self-Adaptive Software Needs Quantitative Verification at Runtime

Human activity increasingly relies on software being able to make self-adaptation decisions. The only way to achieve dependable software adaptation is to unite autonomic computing and mathematically based modeling and analysis techniques. Quantitative verification and model checking must also be used at runtime to predict and identify requirement violations, as well as to plan the adaptation steps necessary to prevent or recover from violations and obtain irrefutable proof the reconfigured software complies with its requirements. In developing a machine, software engineers must first derive a specification from the requirements and so must understand the relevant assumptions to be made about the environment in which the machine is expected to work. Domain assumptions play a fundamental role in building systems. Quantitative verification is a mathematically based technique for analyzing the correctness, performance, and reliability of systems exhibiting stochastic behavior.