Abstract
Formal verification of dynamic, concurrent and real-time systems has been the focus of several decades of software engineering research. Formal verification requires high-performance data processing software for extracting knowledge from the unprecedented amount of data containing all reachable states and all transitions that systems can make among those states, for instance, the extraction of specific reachable states, traces, and more. One of the most challenging task in this context is the development of tools able to cope with the complexity of real-world models analysis. Many methods have been proposed to alleviate this problem. For instance, advanced state space techniques aim at reducing the data needed to be constructed in order to verify certain properties. Other directions are the efficient implementation of such analysis techniques, and studying ways to parallelize the algorithms in order to exploit multi-core and distributed architectures. Since cloud-based computing resources have became easily accessible, there is an opportunity for verification techniques and tools to undergo a deep technological transition to exploit the new available architectures. This has created an increasing interest in parallelizing and distributing verification techniques. Cloud computing is an emerging and evolving paradigm where challenges and opportunities allow for new research directions and applications. There is an evidence that this trend will continue, in fact several companies are putting remarkable efforts in delivering services able to offer hundreds, or even thousands, commodity computers available to customers, thus enabling users to run massively parallel jobs. This revolution is already started in different scientific fields, achieving remarkable breakthroughs through new kinds of experiments that would have been impossible only few years ago. Anyway, despite many years of work in the area of multi-core and distributed model checking, still few works introduce algorithms that can scale effortlessly to the use of thousands of loosely connected computers in a network, so existing technology does not yet allow us to take full advantage of the vast array of compute power of a "cloud" environment. Moreover, despite model checking software tools are so called "push-button", managing a high-performance computing environment required by distributed scientific applications, is far from being considered such, especially whenever one wants to exploit general purpose cloud computing facilities. The thesis focuses on two complementary approaches to deal with the state explosion problem in formal verification. On the one hand we try to decrease the exploration space by studying advanced state space methods for real-time systems modeled with Time Basic Petri nets. In particular, we addressed and solved several different open problems for such a modeling formalism. On the other hand, we try to increase the computational power by introducing approaches, techniques and software tools that allow us to leverage the "big data" trend to some extent. In particular, we provided frameworks and software tools that can be easily specialized to deal with the construction and verification of very huge state spaces of different kinds of formalisms by exploiting big data approaches and cloud computing infrastructures.