From biological systems to cyber-physical systems, monitoring the behavior of such dynamical systems often requires reasoning about complex spatiooral properties of physical and computational entities that are dynamically interconnected and arranged in a particular spatial configuration. Spatiooral Reach and Escape Logic (STREL) is a recent logic-based formal language designed to specify and reason about spatiooral properties. STREL considers each system's entity as a node of a dynamic weighted graph representing its spatial arrangement. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterizing the node's behavior. While there are offline algorithms available for monitoring STREL specifications over logged simulation traces, here we investigate for the first time an online algorithm enabling the runtime verification during the system's execution or simulation. Our approach extends the original framework by considering imprecise signals and by enhancing the logics' semantics with the possibility to express partial guarantees about the conformance of the system's behavior with its specification. Finally, we demonstrate our approach in a real-world environmental monitoring case study.

Online monitoring of spatiooral properties for imprecise signals

Nenzi L.
2021-01-01

Abstract

From biological systems to cyber-physical systems, monitoring the behavior of such dynamical systems often requires reasoning about complex spatiooral properties of physical and computational entities that are dynamically interconnected and arranged in a particular spatial configuration. Spatiooral Reach and Escape Logic (STREL) is a recent logic-based formal language designed to specify and reason about spatiooral properties. STREL considers each system's entity as a node of a dynamic weighted graph representing its spatial arrangement. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterizing the node's behavior. While there are offline algorithms available for monitoring STREL specifications over logged simulation traces, here we investigate for the first time an online algorithm enabling the runtime verification during the system's execution or simulation. Our approach extends the original framework by considering imprecise signals and by enhancing the logics' semantics with the possibility to express partial guarantees about the conformance of the system's behavior with its specification. Finally, we demonstrate our approach in a real-world environmental monitoring case study.
File in questo prodotto:
File Dimensione Formato  
2021_Online Monitoring of SpatioTemporal Properties for Imprecise Signals.pdf

accesso aperto

Descrizione: free at link : https://dl.acm.org/doi/10.1145/3487212.3487344
Licenza: Digital Rights Management non definito
Dimensione 1.91 MB
Formato Adobe PDF
1.91 MB Adobe PDF Visualizza/Apri
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/3005707
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 1
social impact