Synthesis and Verification of Self-aware Computing Systems

Radu Constantin Calinescu; Marco Autili; Javier Cámara; Antinisca Di Marco; Simos Gerasimou; Paola Inverardi; Alexander Perucci; Nils Jansen; Joost-Pieter Katoen; Marta Kwiatkowska; Ole J Mengshoel; Romina Spalazzese; Massimo Tivoli

doi:10.1007/978-3-319-47474-8_11

Synthesis and Verification of Self-aware Computing Systems

Radu Constantin Calinescu, Marco Autili, Javier Cámara, Antinisca Di Marco, Simos Gerasimou, Paola Inverardi, Alexander Perucci, Nils Jansen, Joost-Pieter Katoen, Marta Kwiatkowska, Ole J Mengshoel, Romina Spalazzese, Massimo Tivoli

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

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 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.

Original language	English
Title of host publication	Self-Aware Computing Systems
Publisher	Springer
Pages	337-373
Number of pages	37
ISBN (Print)	9783319474724
DOIs	https://doi.org/10.1007/978-3-319-47474-8_11
Publication status	Published - 2017

Access to Document

10.1007/978-3-319-47474-8_11

http://link.springer.com/chapter/10.1007%2F978-3-319-47474-8_11

Cite this

@inbook{dd7c2fb080db4a6f87d11c15459d2a4e,

title = "Synthesis and Verification of Self-aware Computing Systems",

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 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.",

author = "Calinescu, {Radu Constantin} and Marco Autili and Javier C{\'a}mara and {Di Marco}, Antinisca and Simos Gerasimou and Paola Inverardi and Alexander Perucci and Nils Jansen and Joost-Pieter Katoen and Marta Kwiatkowska and Mengshoel, {Ole J} and Romina Spalazzese and Massimo Tivoli",

year = "2017",

doi = "10.1007/978-3-319-47474-8_11",

language = "English",

isbn = "9783319474724",

pages = "337--373",

booktitle = "Self-Aware Computing Systems",

publisher = "Springer",

address = "Germany",

}

TY - CHAP

T1 - Synthesis and Verification of Self-aware Computing Systems

AU - Calinescu, Radu Constantin

AU - Autili, Marco

AU - Cámara, Javier

AU - Di Marco, Antinisca

AU - Gerasimou, Simos

AU - Inverardi, Paola

AU - Perucci, Alexander

AU - Jansen, Nils

AU - Katoen, Joost-Pieter

AU - Kwiatkowska, Marta

AU - Mengshoel, Ole J

AU - Spalazzese, Romina

AU - Tivoli, Massimo

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-47474-8_11

DO - 10.1007/978-3-319-47474-8_11

M3 - Chapter (peer-reviewed)

SN - 9783319474724

SP - 337

EP - 373

BT - Self-Aware Computing Systems

PB - Springer

ER -