@inproceedings{10.1007/978-3-031-19762-8_7,
title = {Formally Verified Self-adaptation of an Incubator Digital Twin},
author = {Thomas Wright and Cláudio Gomes and Jim Woodcock},
editor = {Tiziana Margaria and Bernhard Steffen},
isbn = {978-3-031-19762-8},
year = {2022},
date = {2022-03-02},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Practice},
pages = {89--109},
publisher = {Springer Nature Switzerland},
address = {Cham},
abstract = {The performance and reliability of Cyber-Physical Systems are increasingly aided through the use of digital twins, which mirror the static and dynamic behaviour of a Cyber-Physical System (CPS) in software. Digital twins enable the development of self-adaptive CPSs which reconfigure their behaviour in response to novel environments. It is crucial that these self-adaptations are formally verified at runtime, to avoid expensive re-certification of the reconfigured CPS. In this paper, we demonstrate formally verified self-adaptation in a digital twinning system, by constructing a non-deterministic model which captures the uncertainties in the system behaviour after a self-adaptation. We use Signal Temporal Logic to specify the safety requirements the system must satisfy after reconfiguration and employ formal methods based on verified monitoring over Flow* flowpipes to check these properties at runtime. This gives us a framework to predictively detect and mitigate unsafe self-adaptations before they can lead to unsafe states in the physical system.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}