Research Article
Automatic verification of reliability requirements of spatio-temporal analysis using Three-Valued Spatio-Temporal Logic
@INPROCEEDINGS{10.4108/eai.5-12-2017.2274459, author={Ludovica Luisa Vissat and Jane Hillston and Michele Loreti and Laura Nenzi}, title={Automatic verification of reliability requirements of spatio-temporal analysis using Three-Valued Spatio-Temporal Logic}, proceedings={11th EAI International Conference on Performance Evaluation Methodologies and Tools}, publisher={ACM}, proceedings_a={VALUETOOLS}, year={2018}, month={8}, keywords={spatio-temporal logics statistical model checking spatial population models}, doi={10.4108/eai.5-12-2017.2274459} }- Ludovica Luisa Vissat
Jane Hillston
Michele Loreti
Laura Nenzi
Year: 2018
Automatic verification of reliability requirements of spatio-temporal analysis using Three-Valued Spatio-Temporal Logic
VALUETOOLS
ACM
DOI: 10.4108/eai.5-12-2017.2274459
Abstract
In this paper we present the recently introduced Three-Valued Spatio-Temporal Logic (TSTL), which extends the available spatio-temporal analysis of stochastic systems, and an automatic procedure to verify whether this analysis satisfies given reliability requirements. The novel spatio-temporal logic TSTL enriches the analysis of properties expressed in Signal Spatio-Temporal Logic (SSTL), providing further insight into the dynamic behaviour of systems. Starting from the estimated satisfaction probabilities of given SSTL properties, it enables the analysis of their temporal and spatial evolution. We use a three-valued approach in our verification procedure to include the uncertainty associated with the simulation-based statistical method used to estimate the satisfaction probabilities. In relation to this aspect, we introduce a reliability specification for the TSTL analysis and we present a specific algorithm to automatically assess whether it is satisfied by the evaluation of TSTL formulas.