The recent extensive availability of 'cloud' computing platforms is very appealing for the formal verification community. In fact, these platforms represent a great opportunity to run massively parallel jobs and analyze 'big data' problems, although classical formal verification tools and techniques must undergo a deep technological transformation to take advantage of the available powerful architectures. A distributed approach to verification of computation tree logic formulas on very large state spaces is described. The approach exploits and integrates our parametric state-space builder, designed to ease the adoption of 'big data' platforms. The whole framework adopts a MAPREDUCEapproach as the core computational model and can be tailored to different modeling formalisms. This paper includes proofs of correctness, a short theoretical discussion about complexity, and reports a practical experience with some benchmarking Petri net models. The outcomes of several tests are presented, thus showing the convenience of the proposed approach.
Distributed CTL model checking using MapReduce : theory and practice / C. Bellettini, M. Camilli, L. Capra, M. Monga. - In: CONCURRENCY AND COMPUTATION. - ISSN 1532-0626. - 28:11(2016), pp. 3025-3041.
Distributed CTL model checking using MapReduce : theory and practice
C. BellettiniPrimo
;M. Camilli;L. CapraPenultimo
;M. MongaUltimo
2016
Abstract
The recent extensive availability of 'cloud' computing platforms is very appealing for the formal verification community. In fact, these platforms represent a great opportunity to run massively parallel jobs and analyze 'big data' problems, although classical formal verification tools and techniques must undergo a deep technological transformation to take advantage of the available powerful architectures. A distributed approach to verification of computation tree logic formulas on very large state spaces is described. The approach exploits and integrates our parametric state-space builder, designed to ease the adoption of 'big data' platforms. The whole framework adopts a MAPREDUCEapproach as the core computational model and can be tailored to different modeling formalisms. This paper includes proofs of correctness, a short theoretical discussion about complexity, and reports a practical experience with some benchmarking Petri net models. The outcomes of several tests are presented, thus showing the convenience of the proposed approach.File | Dimensione | Formato | |
---|---|---|---|
Bellettini_et_al-2015-Concurrency_and_Computation-_Practice_and_Experience.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
913.02 kB
Formato
Adobe PDF
|
913.02 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.