The STARK tool
The Software Tool for the Analysis of Robustness in the unKnown environment (STARK) is a Java tool for the specification, analysis and verification of robustness properties of cyber-physical systems that is based on the evolution sequence model from [1] for the representation of systems behaviour, and on the Robustness Temporal Logic (RobTL) from [2] for the specification of robustness properties.
STARK, available on GitHub, consists of a front-end and a Java library, and offers:
A domain specific language for the specification of systems (agents, environment, and their interaction), perturbations, distance expressions, and RobTL formulae;
A module for the simulation of evolution sequences and their perturbed versions;
A module for the evaluation of distances between evolution sequences;
A statistical model checker for RobTL formulae, with either Boolean or three-valued evaluation.
An overview of the tool can be found in [3], and their detailed description is given at https://github.com/quasylab/jspear/wiki
[1] Valentina Castiglioni, Michele Loreti, and Simone Tini. "A framework to measure the robustness of programs in the unpredictable environment".
Logical Methods in Computer Science vol. 19(3), 2023.Â
https://doi.org/10.46298/lmcs-19(3:2)2023
[2] Valentina Castiglioni, Michele Loreti, and Simone Tini. "RobTL: A temporal logic for the robustness of cyber-physical systems".
Available at https://doi.org/10.48550/arXiv.2212.11158
[3] Valentina Castiglioni, Michele Loreti, and Simone Tini. "STARK: A Software Tool for the Analysis of Robustness in the unKnown environment".
Proceedings of COORDINATION 2023, Lecture Notes in Computer Science vol. 13908, pp 115--132, 2023.