ABSTRACT
This chapter focuses on its application in the verification of distributed concurrent software systems. It provides an overview of formal verification of distributed concurrent systems through model checking, which evaluates whether or not a property holds on the model corresponding to the practical system by exhaustively exploring the state space. The chapter presents how the well-known limits of software testing techniques can be addressed by means of formal verification. When a distributed concurrent system has been designed and implemented, software testing techniques can be applied to check whether it works as expected or not. Model checking aims at proving that the property of interest holds by exhaustively exploring every possible state the system under analysis can reach during its execution, starting from its initial state. Time and memory resources to be used during verification are always a critical issue, common to all model checkers.
