Three Case Studies on Verification of Infinite-State Systems

Most software systems have an infinite number of reachable states due to variables with unbounded data domains, parameters, control structures, time, or communication mechanisms based on buffers or queues. Each of these sources of infinity has been studied using formal models such as timed automata, channel systems, extensions of Petri nets, pushdown processes, broadcast protocols, counter automata, different process algebras, or rewrite systems. This paper is a modest attempt at describing underlying connections by introducing the key concept of symbolic search in a very general framework, along with the conditions for turning it into an effective algorithm. Papers at conferences usually follow a horizontal approach: They may present a decidability result, leaving an efficient algorithm for further research, or vice versa. Or they may describe an implementation and report on experimental results, without presenting the underlying theory, and without explaining the steps from the system to a formal model. In contrast, we present three case studies following a vertical approach: First, a verification challenge is informally described; then, a formal model of the system is presented; after that, the theory of symbolic search for an adequate class of models is developed, and, finally, the algorithm is executed on a formal model. The concrete case studies are: A mutex protocol modeled as timed automaton, a cache-coherence protocol modeled as a linear automaton, and a skyline plotter modeled as a pushdown automaton.