jSSTL - A tool to monitor spatio-temporal properties

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.