tion to execute effectively. Adaptation
becomes much more of an inter-level
problem than a set of isolated intra-level solutions.
Cloud infrastructures also impose
a shift from client-side, proprietary
computing resources to shared resources. Web services forced software
engineers to address the distributed
ownership of their applications; the
cloud is now forcing them to address
the distributed ownership of the infrastructure used to run their applications. To some extent, problems associated with distributed ownership
are already considered by application
developers using services run and
shared by others. Clouds complicate
such problems significantly, with execution of one application competing
against execution of another, turning self-verification and self-adaption
into infrastructurewide requirements.
We discussed the runtime use of quantitative verification and model checking as ways to obtain dependable self-adaptive software. Our experience on a
range of projects shows that quantitative verification at runtime can support
software adaptation by identifying
and, sometimes, predicting requirement violations; supporting rigorous
planning of the reconfiguration steps
self-adaptive software employs to recover from such requirement violations; and providing irrefutable proof
the selected reconfiguration steps are
correct. The result is software supporting not only automated changes
but their continual formal analysis to
verify that software continues to meet
requirements as it evolves.
This research was partially funded by the European Commission
Programme IDEAS-ERC, Project
227977-SMScom, by the U.K. Engineering and Physical Sciences Research Council Grants EP/F001096/1
and EP/H042644/1, by the European
Commission FP 7 project CONNECT
(IST 231167), and by the ERC Advanced Grant VERIWARE.
1. allan, C., avgustinov, p., Christensen, a.s., hendren,
l., Kuzins, s., lhotak, o., de Moor, o., sereni, D.,
sittampalam, g., and tibble, J. adding trace
matching with free variables to aspectJ. In
Proceedings of the 20th Annual ACM SIGPLAN
Conference on Object-Oriented Programming,
Systems, Languages, and Applications (san Diego,
oct. 16–20). aCM press, new york, 2005, 345–364.
Radu Calinescu ( radu.Calinescu@york.ac.uk) is a
senior lecturer in large-scale complex It systems in the
Department of Computer science, university of york, u.K.
Carlo Ghezzi ( Carlo.email@example.com) is a professor
and chair of software engineering in the Dipartimento di
elettronica e Informazione, politecnico di Milano, Italy,
and president of Informatics europe.
Marta Kwiatkowska ( Marta.Kwiatkowska@cs.ox.ac.uk)
is a professor of computing systems and fellow of trinity
College, university of oxford, u.K.
Raffaela Mirandola ( firstname.lastname@example.org) is an
associate professor in the Dipartimento di elettronica e
Informazione, politecnico di Milano, Italy.
© 2012 aCM 0001-0782/12/09 $15.00