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 a detailed description is in the proper wiki .
Digital-Twin STARK [4,6] extends STARK with feedback, a mechanism that allow us to model the communications, and their effects, between the digital and the physical (perturbed) twin in a concise, clean fashion. The features of Stark allows us to compare the behaviour of the twins, to verify properties over them, and to measure effectiveness.
Bio-STARK [5] extends the core of STARK by refining the discrete step modelling into a time point modelling. It allows us to verify robustness properties in systems biology, by capturing the effects of (unpredictable) perturbations on species in biochemical networks, as well as on the oscillatory behaviour of gene regulatory networks
[1] V. Castiglioni, M. Loreti, S. Tini:
A framework to measure the robustness of programs in the unpredictable environment
Logical Methods in Computer Science 19(3), 2:1-2:46 (2023)
[2] V. Castiglioni, M. Loreti, S. Tini:
RobTL: Robustness Temporal Logic for CPS
CONCUR 2024. LIPIcs 311, 2024, 15.
[3] V. Castiglioni, M. Loreti, S. Tini:
STARK: A tool for the analysis of CPSs robustness
Science of Computer Programming 236: 103134 (2024).
[4] V. Castiglioni, R. Lanotte, M. Loreti, S. Tini:
Evaluating the Effectiveness of Digital Twins Through Statistical Model Checking with Feedback and Perturbations
FMICS 2024, LNCS 14952.
[5] V. Castiglioni, M. Loreti, S. Tini:
Bio-Stark: A Tool for the Time-Point Robustness Analysis of Biological Systems
CMSB 2024, LNCS 14971
[6] V. Castiglioni, R. Lanotte, M. Loreti, S. Tini:
DT-STARK: A Tool for Evaluating the Effectiveness of Digitsl Twins throuhg Feedback and Perturbations.
Int. J. Softw. toold Technol. Transf. 25(5): 443-464.