Synthesis and verification of self aware systems
Self aware computing systems are envisaged to exploit the knowledge of their own software architecture, hardware infrastructure and environment in order to follow high level goals through proactively adapting as their environment evolves. This chapter describes two classes of key enabling techniques for self adaptive systems: automated synthesis and formal verification. The ability to dynamically synthesise component connectors and compositions underpins the proactive adaptation of the architecture of self aware systems. Deciding when adaptation is needed and selecting valid new architectures or parameters for self aware systems often requires formal verification. We present the state of the art in the use of the two techniques for the development of self aware computing systems, and summarise the main research challenges associated with their adoption in practice. Radu Calinescu University of York, UK, e mail: radu.calinescu@york.ac.uk Marco Autili University of L'Aquila, Italy, e mail: marco.autili@univaq.it Javier Camara Carnegie Mellon University, US, e mail: jcmoreno@cs.cmu.edu Antinisca Di Marco University of L'Aquila, Italy, e mail: antinisca.dimarco@univaq.it Simos Gerasimou University of York, UK, e mail: simos@cs.york.ac.uk Paola Inverardi University of L'Aquila, Italy, e mail: paola.inverardi@univaq.it Alexander Perucci University of L'Aquila, Italy, e mail: alexander.perucci@graduate.univaq.it Nils Jansen University of Texas at Austin, US, e mail: njansen@utexas.edu Joost Pieter Katoen RWTH Aachen University, Germany, e mail: katoen@cs.rwth aachen.de Marta Kwiatkowska University of Oxford, UK, e mail: marta.kwiatkowska@cs.ox.ac.uk Ole J Mengshoel Carnegie Mellon University, US e mail: ole.mengshoel@sv.cmu.edu Romina Spalazzese Malmo University, Sweden, e mail: romina.spalazzese@mah.se Massimo Tivoli University of L'Aquila, Italy, e mail: massimo.tivoli@univaq.it