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. © 2017 ACM.

Automatic verification of reliability requirements of spatio-temporal analysis using three-valued spatio-temporal logic

Vissat, Ludovica Luisa;Nenzi, Laura
2017-01-01

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. © 2017 ACM.
2017
9781450363464
https://dl.acm.org/citation.cfm?doid=3150928.3150961
File in questo prodotto:
File Dimensione Formato  
Vissat et al. - Automatic verification of reliability requirements.pdf

Accesso chiuso

Descrizione: toc proceeding al link:https://dl.acm.org/citation.cfm?doid=3150928.3150961
Tipologia: Documento in Versione Editoriale
Licenza: Copyright Editore
Dimensione 469.63 kB
Formato Adobe PDF
469.63 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11368/2939428
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact