We present DT-Stark, an extension of the Stark tool aimed at the verification and evaluation of the effectiveness of digital twins, i.e., their ability to direct the physical counterparts. To this end, we introduce feedback in Stark, 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.
Evaluating the Effectiveness of Digital Twins Through Statistical Model Checking with Feedback and Perturbations
Castiglioni V.;Loreti M.;Tini S.
2024-01-01
Abstract
We present DT-Stark, an extension of the Stark tool aimed at the verification and evaluation of the effectiveness of digital twins, i.e., their ability to direct the physical counterparts. To this end, we introduce feedback in Stark, 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
