Ameliorating the state explosion problem.

摘要

Systems that maintain an ongoing interaction with their environment, such as Operating Systems Network Protocols and Microcontrollers, are commonplace. The complexity of these systems necessitates a rigorous verification of correct behavior. Automatic verification methods such as Model Checking, while theoretically efficient, suffer in practice from the large state space of these systems, a phenomenon called State Explosion. State explosion often arises when verifying systems parameterized by the number of component processes, and single systems with large data domains. The main contribution of this dissertation is in the development of abstraction methods that serve to ameliorate the state explosion problem for such systems.; The first part of the dissertation presents abstractions for interesting classes of parameterized systems that reduce the infinite family of instances to a finite-state system, while exactly preserving correctness properties. For parameterized ring systems with a synchronizing token, it suffices to examine a few small instances in order to determine the correctness of every instance of the system. The method is applicable to protocols such as mutual exclusion and Milner's Cycler. Somewhat surprisingly, the verification problem is undecidable even if the token carries a single bit of information. For parameterized synchronous systems, an exact abstraction reduces the parameterized system to a finite "abstract" graph. This abstraction method is applied to the verification of the SAE-J1850 industrial standard bus arbitration protocol. We also present a general algorithm schema from which algorithms for model-checking several types of infinite-state systems can be derived.; The second part of the dissertation presents a proof technique for showing that two programs are equivalent up to "stuttering" (repetition) of states. Stuttering arises when comparing programs that are at different levels of abstraction. The new formulation replaces the global reasoning of earlier techniques with local reasoning, which considerably simplifies abstraction proofs. This new formulation is used in conjunction with a theorem prover to verify a data abstraction for the alternating-bit protocol.