We present the Software Tool for the Analysis of Robustness in the unKnown environment (STARK), our Java tool for the specification, analysis and verification of robustness properties of Cyber-Physical Systems (CPSs). STARK includes: (i) a specification language for systems behaviour, perturbations, distances on systems behaviours, and requirements on systems behaviour expressed in the Robustness Temporal Logic (RobTL), a temporal logic for the specification and verification of properties on the evolution of distances between the behaviours of CPSs, and thus also of robustness properties; (ii) a module for the simulation of system behaviours and their perturbed versions; (iii) a module for the evaluation of distances between behaviours; (iv) a statistical model checker for RobTL formulae.
STARK: A tool for the analysis of CPSs robustness
Castiglioni V.;Loreti M.;Tini S.
2024-01-01
Abstract
We present the Software Tool for the Analysis of Robustness in the unKnown environment (STARK), our Java tool for the specification, analysis and verification of robustness properties of Cyber-Physical Systems (CPSs). STARK includes: (i) a specification language for systems behaviour, perturbations, distances on systems behaviours, and requirements on systems behaviour expressed in the Robustness Temporal Logic (RobTL), a temporal logic for the specification and verification of properties on the evolution of distances between the behaviours of CPSs, and thus also of robustness properties; (ii) a module for the simulation of system behaviours and their perturbed versions; (iii) a module for the evaluation of distances between behaviours; (iv) a statistical model checker for RobTL formulae.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
