We present an approach for the automated formal verification of distributed systems based on the Storm technology. The approach is based on a formal model of the behavior of Storm topologies given in terms of the CLTLoc metric temporal logic extended with counters. We present a tool-supported mechanism to automatically generate formal models from high-level description of Storm topologies. The Zot formal verification tool is then used to check whether some desired properties hold for the modeled system or not. The analyzed properties concern the growth of the queues of the nodes of the Storm topology. Some experiments performed on example topologies show how the timing features of the modeled system influence the behavior of the queues of the nodes.

Towards the formal verification of data-intensive applications through metric temporal logic

MARCONI, FRANCESCO;BERSANI, MARCELLO MARIA;ROSSI, MATTEO GIOVANNI
2016-01-01

Abstract

We present an approach for the automated formal verification of distributed systems based on the Storm technology. The approach is based on a formal model of the behavior of Storm topologies given in terms of the CLTLoc metric temporal logic extended with counters. We present a tool-supported mechanism to automatically generate formal models from high-level description of Storm topologies. The Zot formal verification tool is then used to check whether some desired properties hold for the modeled system or not. The analyzed properties concern the growth of the queues of the nodes of the Storm topology. Some experiments performed on example topologies show how the timing features of the modeled system influence the behavior of the queues of the nodes.
2016
International Conference on Formal Engineering Methods
9783319478456
9783319478456
Data-intensive applications; Distributed systems; Formal verification; Metric temporal logic; Storm technology; Theoretical Computer Science; Computer Science (all)
File in questo prodotto:
File Dimensione Formato  
chp%3A10.1007%2F978-3-319-47846-3_13.pdf

Accesso riservato

Descrizione: Versione pubblicata
: Publisher’s version
Dimensione 1.04 MB
Formato Adobe PDF
1.04 MB Adobe PDF   Visualizza/Apri
main.pdf

Open Access dal 19/11/2017

Descrizione: Versione accettata
: Post-Print (DRAFT o Author’s Accepted Manuscript-AAM)
Dimensione 746.46 kB
Formato Adobe PDF
746.46 kB Adobe PDF Visualizza/Apri

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/11311/1005783
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 4
social impact