Data di Pubblicazione:
2016
Citazione:
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.
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.
Tipologia IRIS:
01 - Articolo su periodico
Keywords:
Cloud computing; CTL; Distributed algorithms; Formal verification; MapReduce; Computer Networks and Communications; Computer Science Applications1707 Computer Vision and Pattern Recognition; Software; Computational Theory and Mathematics; Theoretical Computer Science
Elenco autori:
C. Bellettini, M. Camilli, L. Capra, M. Monga
Link alla scheda completa: