Iterative methods for formal verification of digital systems
Felice Balarin · 1995
Complexity management is the key to applying formal verification methods to real-life digital designs. Abstractions are a powerful tool to manage complexity, but finding a useful abstraction is a difficult task requiring significant designer's effort. In this work I propose techniques for automatic abstraction for three classes of systems: networks of communicating finite-state machines, real-time systems and arrays of identical components. I show that ignoring communication in a network of finite-state machines can be used to simplify the representation of the system. Ignoring communication can prove to be too simplistic. In that case communication is selectively restored. The process is repeated until a suitable abstraction is found. I show that the process terminates in finitely many iterations. We also develop a similar approach for real-time systems. All timing constraints are initially relaxed, and if that abstraction is proven too simplistic, then some of them are enforced. Again, the process is iterated. I consider two models of real-time systems: a basic model of real-time systems, called timed automata and propose an extended one called timed automata with decrements (TAD's) that allows modeling some high-level features of systems (e.g. interrupts) that can not be modeled accurately with timed automata. I show that the proposed iterative process always terminates for timed automata, while it may not terminate for arbitrary TAD's. I also show that this limitation is intrinsic, because the verification problem is undecidable for TAD's. Finally, I will show how to select automatically a subset of timing constraints necessary to verify a real-time system. Since typically only a small fraction of timing constraints is relevant to any given property, eliminating the rest of the constraints can improve the efficiency of the verification process dramatically. Finally, for arrays of identical components I address the problem of finding an abstraction which is independent of the actual number of components. Such an abstraction can then be used to verify a whole class of arrays of different sizes. I show that the problem is undecidable in general, and propose some search strategies that can find such an abstraction in special cases.