Oxford logo
[Calinescu2017] R. Calinescu, M. Autili, J. Camara, A. Di Marco, S. Gerasimou, P. Inverardi, A. Perucci, N. Jansen, J.-P. Katoen, M. Kwiatkowska, O. J. Mengshoel, R. Spalazzese and M. Tivoli. Synthesis and Verification of Self-aware Computing Systems. In S. Kounev, J. O. Kephart, A. Milenkoski and X. Zhu (editors), Self-Aware Computing Systems, pages 337-373, Springer International Publishing. 2017. [pdf] [bib]
Downloads:  pdf pdf (1.6 MB)  bib bib
Notes: The original publication is available at link.springer.com.
Abstract. 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.