Techniques for verification of infinite state systems
C. R. Ramakrishnan, Samik Basu · 2003
Ensuring reliability and security of software are important concerns in a software development process. Formal methods offer a promising approach for specifying and verifying such critical behaviors of software. Many software systems, in our day-to-day computing world, are inherently infinite state where infiniteness arises due to the presence of (a) infinite data domains (message-passing), (b) infinite control behavior (recursions) and (c) infinite number of sub-systems (replications). In this context, we explore different formal techniques for automatically verifying systems such that infiniteness in system behavior is handled in a fashion directly addressing its cause. The thesis is broadly organized in three parts as follows. In the first part, we introduce the notion of symbolic transition systems (STS), a generalized representation technique for systems with infinite data domain. Verification of such systems is then performed using bisimulation equivalence by symbolically manipulating the infinite domain variables present in the system. We show the power and versatility of tabled-constraint logic program in naturally encoding local bisimulation checker for STS. The second part deals with programs with (recursive) procedure calls. Abstract models of such programs exhibit infinite control behavior due to unbounded recursion depth. We introduce the concept of resource-constraint where resource refers to the size of stack used by the program. We implemented resource-constrained model checker for recursive programs which automatically discards all infeasible stack divergence traces of the program and reasons about program execution with finite depth stack. Finally, in the third part, we consider parameterized systems which are infinite family of (typically) finite state systems. The goal of verification of parameterized systems is to check properties that are satisfied or dissatisfied by each and every member of the infinite family. We propose a new verification technique based on compositional analysis to reason about such systems. Our verification procedure is independent of the system topology (inter-connection pattern) and requires no user guidance. We show the usefulness of our technique by presenting its application in verifying typical parameterized systems like token-passing protocol, multi-threaded locking systems and multi-processor cache coherence protocol.