Parallel Analysis with FAMVal to Speed Up Simulation-based Model Checking

While model checking is a powerful technique to analyze the properties of a model, it can be very expensive or even impossible, if the model comprises many states that have to be explored. Simulation-based model checking is an alternative, where the properties defined in temporal logics are not checked on the model itself but on traces produced during model execution. However, for stochastic models multiple traces have to be considered. A natural way to increase the efficiency of the analysis of a set of traces is to distribute the analysis runs among a set of computational resources. These resources can be the local cores of a multi-core CPU as well as a computer network. We extended FAMVal (Flexible Architecture for Model Validation) to execute analysis tasks in a parallel and distributed manner and supports the parallelization on both - local multicore machines as well as networks. Furthermore, it allows an exchange of the underlying simulation tool, and arbitrary analysis methods. Experiments based on the modeling and simulation framework James II and with a Wnt/β-catenin signaling pathway model illustrate the efficiency of parallel simulation-based model checking in FAMVal.