The recent extensive availability of 'big data' platforms calls for a widespread adoption by the formal verification community. Cloud computing platforms represent a great opportunity to run massively parallel jobs, yet classical formal verification tools/techniques must undergo a deep technological transformation in order to exploit the new available architectures. This has raised an increasing interest in deploying verification techniques on parallel/distributed frameworks. In this paper we introduce a framework to ease the adoption of a distributed approach to verification of Computation Tree Logic (CTL) formulas on very large state spaces. The approach exploits/integrates a recently developed, parametric state-space builder. The whole framework adopts M AP R EDUCE as core computational model, and can be tailored to different modelling formalisms. The outcomes of several tests performed on (Petri-nets based) benchmark specifications are presented, thus showing the convenience of the proposed approach.
CTL model checking in the cloud using MapReduce / M. Camilli, C. Bellettini, L. Capra, M. Monga - In: 16. International symposium on symbolic and numeric algorithms for scientific computing : SYNASC 2014 : 22-25 September 2014, Timisoara, Romania : proceedings / [a cura di] F. Winkler, V. Negru, T. Ida, T. Jebelean, D. Petcu, S. Watt, D. Zaharie. - Piscataway (New Jersey) : IEEE Computer society, 2015 Feb. - ISBN 9781479984480. - pp. 333-340 (( Intervento presentato al 16. convegno International symposium on symbolic and numeric algorithms for scientific computing (SYNASC) tenutosi a Timisoara (Romania) nel 2014 [10.1109/SYNASC.2014.52].
CTL model checking in the cloud using MapReduce
M. CamilliPrimo
;C. BellettiniSecondo
;L. CapraPenultimo
;M. MongaUltimo
2015
Abstract
The recent extensive availability of 'big data' platforms calls for a widespread adoption by the formal verification community. Cloud computing platforms represent a great opportunity to run massively parallel jobs, yet classical formal verification tools/techniques must undergo a deep technological transformation in order to exploit the new available architectures. This has raised an increasing interest in deploying verification techniques on parallel/distributed frameworks. In this paper we introduce a framework to ease the adoption of a distributed approach to verification of Computation Tree Logic (CTL) formulas on very large state spaces. The approach exploits/integrates a recently developed, parametric state-space builder. The whole framework adopts M AP R EDUCE as core computational model, and can be tailored to different modelling formalisms. The outcomes of several tests performed on (Petri-nets based) benchmark specifications are presented, thus showing the convenience of the proposed approach.File | Dimensione | Formato | |
---|---|---|---|
articolo.pdf
accesso riservato
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
363.36 kB
Formato
Adobe PDF
|
363.36 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.