Distributed CTL model checking using MapReduce: theory and practice. (20th September 2015)

• Record Type: Journal Article
• Authors: Bellettini, Carlo; Camilli, Matteo; Capra, Lorenzo; Monga, Mattia
• Other Names: Frincu Mark guestEditor.; Bósa Károly guestEditor.; Rong Chunming guestEditor.; Liu Lu guestEditor.; Chen Guolong guestEditor.
• Is Part Of: Concurrency and computation. Volume 28:Number 11(2016)
• Page Start: 3025
• Page End: 3041
• Publication Date: 2015-09-20
• Subjects: formal verification -- CTL -- distributed algorithms -- cloud computing -- MapReduce; Parallel processing (Electronic computers) -- Periodicals; Parallel computers -- Periodicals; 004.35
• DOI: 10.1002/cpe.3652
• Languages: English
• ISSNs: 1532-0626

Abstract

Summary: 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 aMAPREDUCE approach 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. Copyright © 2015 John Wiley & Sons, Ltd.