25 years of model checking

Abstract

Model Checking is an automatic verification technique for large state transition systems. It was originally developed for reasoning about finite-state concurrent systems. The technique has been used successfully to debug complex computer hardware, communication protocols, and software. It is beginning to be used for analyzing cyberphysical, biological, and financial systems as well. The major challenge for the technique is a phenomenon called the State Explosion Problem. This issue is impossible to avoid in the worst case; but, by using sophisticated data structures and clever search algorithms, it is now possible to verify state transition systems with an astronomical number of states. In this paper, we will briefly review the development of Model Checking over the past 32 years, with an emphasis on model checking stochastic hybrid systems.