DT-Stark: a tool for evaluating the effectiveness of digital twins through feedback and perturbations

A digital twin is a virtual replica of a physical system that has to interact with it in real-time in order to facilitate decision-making, to reduce failures and costs, and to ensure a coherent and safe system execution. We call effectiveness the ability of the digital twin to direct the physical counterpart. In this paper we provide the means to evaluate the effectiveness of a digital twin in the case that the physical system is operating under uncertainty, and it is therefore subject to perturbations. Specifically, we present the DT-Stark tool, that extends Stark, a tool for modelling and verification of systems operating under uncertainty, with feedback, a special mechanism that allow us to model the communications, and their effects, between the digital and the physical (perturbed) twin in a concise, clean fashion. We can then exploit the features of Stark to compare the behaviour of the twins, to verify properties over them, and to measure effectiveness. We provide some examples of the use of our tool by applying it to the evaluation of the effectiveness of digital twins in two robotic scenarios: an industrial plant and a smart hospital.