text: 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.
  @cite_24: As model checking becomes increasingly used in industry, there is a big need for efficient new methods to deal with the large real-size designs. The author presents a novel method for improving the performance of model checking using parallelisation techniques. The model checking is performed on a distributed-memory environment consisting of a network of machines. The important two keys to focus on are the memory balance and communication reduction. A new algorithm for partitioning the large state space modelling industrial designs with hundreds of millions of states and transitions is proposed. The state space is supposed to be represented by a weighted Kripke structure (this is an extension of the Kripke structure where weights are associated with the states and with the transitions). This algorithm partitions the weighted Kripke structure by performing a combination of abstraction-partition-refinement on this structure. The CTL model checking algorithm is distributed on processes located on different network machines. Each one owns a partition and executes the algorithm on it. The algorithm for CTL model checking is designed to reduce the communication overhead between the processes. The experimental results on large real designs show that this method improves the quality of partitions, the communication overhead and then the overall performance of the model checking.
  @cite_19: With the use of state and memory reduction techniques in verification by explicit state enumeration, runtime becomes a major limiting factor. We describe a parallel version of the explicit state enumeration verifier Murφ for distributed memory multiprocessors and networks of workstations that is based on the message passing paradigm. In experiments with three complex cache coherence protocols, parallel Murφ shows close to linear speedups, which are largely insensitive to communication latency and bandwidth. There is some slowdown with increasing communication overhead, for which a simple yet relatively accurate approximation formula is given. Techniques to reduce overhead and required bandwidth and to allow heterogeneity and dynamically changing load in the parallel machine are discussed, which we expect will allow good speedups when using conventional networks of workstations.
  @cite_29: The main limiting factor of the model checker SPIN is currently the amount of available physical memory. This paper explores the possibility of exploiting a distributed-memory execution environment, such as a network of workstations interconnected by a standard LAN, to extend the size of the verification problems that can be successfully handled by SPIN. A distributed version of the algorithm used by SPIN to verify safety properties is presented, and its compatibility with the main memory and complexity reduction mechanisms of SPIN is discussed. Finally, some preliminary experimental results are presented.
  @cite_5: In this paper we propose a distributed algorithm for model-checking LTL formulas that works on a network of workstations and effectively uses the decomposition of the formula automaton to strongly connected components to achieve more efficient distribution of the verification problem. In particular, we explore the possibility of performing a distributed nested depth-first search algorithm.
summary: The main idea of distributed algorithms for both LTL and CTL model checking is in fact similar: the state graph is partitioned among the network nodes, each network node owns a subset of the state space. The differences are in the way the state space is partitioned (through a ): this is a crucial issue. In order to increase performance of the parallel model checking, it is key to achieve a good load balancing among machines, meaning that each partition should contain nearly the same number of states. The performance of these algorithms depends also on the number of cross-border transitions of the partitioned state space ( transitions having the source state in a component and the target state in another component). This number should be as small as possible, since it has an effect on the number of messages sent over the network during the analysis @cite_24 . In the context of LTL model checking, probabilistic techniques to partition the state space have been used, for example, in @cite_29 @cite_19 , and a technique that exploits some structural properties derived from the verified formula has been proposed in @cite_5 .