Synthesis and verification of delf-aware computing systems - Calinescu, R; Autili, M; Camara, J; Di Marco, A; Gerasimou, S; Inverardi, P; Perucci, A; Jansen, N; Katoen, J; Kwiatkowska, M; Mengshoel, O; Spalazzese, R; et al. (Springer, 2017)
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 synthesize 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 summarize the main research challenges associated with their adoption in practice.