We present our efforts on the formalization and automated formal verification of data-intensive applications based on the Storm technology, a well known and pioneering framework for developing streaming applications. The approach is based on the so-called array-based systems formalism, introduced by Ghilardi et al., a suitable abstraction of infinite-state systems that we used to model the runtime behavior of Storm-based applications. The formalization consists of quantified formulae belonging to a certain fragment of first-order logic to symbolically represent array-based systems.The formalization consists of quantified first-order formulae symbolically representing array-based systems. The verification consists in checking whether some safety property holds or not for the system. Both formalization and verification are performed in the same framework, namely the state-of-the-art Cubicle model checker.
Formal verification of data-intensive applications through model checking modulo theories / M.M. Bersani, F. Marconi, M. Rossi, M. Erascu, S. Ghilardi - In: SPIN 2017 : Proceedings[s.l] : ACM, 2017. - ISBN 9781450350778. - pp. 98-101 (( Intervento presentato al 24. convegno SIGSOFT tenutosi a Santa Barbara nel 2017.
Formal verification of data-intensive applications through model checking modulo theories
S. GhilardiUltimo
2017
Abstract
We present our efforts on the formalization and automated formal verification of data-intensive applications based on the Storm technology, a well known and pioneering framework for developing streaming applications. The approach is based on the so-called array-based systems formalism, introduced by Ghilardi et al., a suitable abstraction of infinite-state systems that we used to model the runtime behavior of Storm-based applications. The formalization consists of quantified formulae belonging to a certain fragment of first-order logic to symbolically represent array-based systems.The formalization consists of quantified first-order formulae symbolically representing array-based systems. The verification consists in checking whether some safety property holds or not for the system. Both formalization and verification are performed in the same framework, namely the state-of-the-art Cubicle model checker.File | Dimensione | Formato | |
---|---|---|---|
SPIN17.pdf
accesso riservato
Tipologia:
Pre-print (manoscritto inviato all'editore)
Dimensione
696.89 kB
Formato
Adobe PDF
|
696.89 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.