STARK: A tool for the analysis of CPSs robustness

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.