Controlling and designing spatio-temporal behaviours requires proper formal tools to describe such properties, and to monitor and verify whether, and how robustly, they are satisfied by a system. In this paper, we introduce jSSTL, a Java tool for the specification of Signal Spatio-Temporal Logic (SSTL) properties and their robust monitoring on spatio-temporal trajectories. The tool consists of a jSSTL API and a front-end, integrated in ECLIPSE. We describe in details the framework and the use of the plugin, exploiting a running example of a cholera outbreak.
jSSTL - A tool to monitor spatio-temporal properties
Bortolussi L;
2017
Abstract
Controlling and designing spatio-temporal behaviours requires proper formal tools to describe such properties, and to monitor and verify whether, and how robustly, they are satisfied by a system. In this paper, we introduce jSSTL, a Java tool for the specification of Signal Spatio-Temporal Logic (SSTL) properties and their robust monitoring on spatio-temporal trajectories. The tool consists of a jSSTL API and a front-end, integrated in ECLIPSE. We describe in details the framework and the use of the plugin, exploiting a running example of a cholera outbreak.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
