Conformance Testing and Error Explanation for Software Models

The ever-increasing reliance on digital systems has dramatically increased the emphasis on the reliability of the software controlling them. Consequently, techniques known as formal methods have been developed to mathematically verify correctness of software, and to fix bugs that are found. In general, verification is a hard problem, because of the inherent complexity of abstractions that are used to model programs. For many classes of systems, the verification problem is in fact undecidable (there is no algorithm that can always give the correct answer for arbitrary inputs). Despite these negative results, the urgent need for software validation has fueled research aimed at identifying the largest possible classes for which the problem is not only decidable, but tractable. The first part of this thesis focuses on an important category of software verification problems known as conformance testing. Given a specification of correctness, the problem is to devise a test suite (known as a conformance test) that will pass precisely those program implementations that conform to the specification. We tackle this problem for finite-state models which capture non-recursive programs, and also for pushdown models which capture recursive program behavior. The conformance test must be constructed without knowledge of the program implementation details. For finite-state models, this essentially reduces the problem to exploring an unknown directed graph. The hardness of this latter problem is a well-studied consequence of so-called combination locks, that inhibit exploration algorithms. Our key observation is that the assumptions leading directly to the hardness of conformance testing can, in many cases, be relaxed sufficiently to make the problem tractable. To show this, we establish an interesting connection between three quantities: the number of faults in the program implementation P, the size of certain cuts in the directed graph GP corresponding to P, and the time needed to explore GP via random walks. This result, which we believe is interesting in a far more general context as well, enables us to extend the applicability of conformance testing to a much wider class of program models. For pushdown models, several complications arise because the most well-studied kinds of pushdown automata do not share several key decidability properties enjoyed by finite automata. We focus our attention on the recently proposed sub-class of visibly pushdown automata (VPA) that are powerful enough to capture recursive program behavior and also possess the requisite decidability properties. In order to extend conformance testing algorithms for finite automata to VPAs, we first present a congruence-based characterization of the class of languages accepted by VPAs (similar to the Myhill-Nerode theorem for regular languages). This result has several applications, and in this thesis we apply it to construct conformance tests for VPA program models. While conformance testing is concerned with detecting faults in a program model, error explanation addresses the question of how to correct faults. By its very nature, error explanation is an informal process that admits many heuristics. As a result, there has been very little effort to characterize the complexity of the error explanation problem. Because this is a vital part of any verification endeavor, we address these unanswered questions in the latter half of this thesis. We consider two of the most popular heuristics employed in error-explanation algorithms, and analyze their complexity as a function of the program model. We establish an interesting connection between error explanation according to one heuristic, and the problem of determining the smallest deterministic finite automaton that is consistent with a given sample of positively and negatively labeled inputs. By appealing to a well-known hardness result for this latter problem, we are able to show that this approach to error explanation is likely to be intractable. On the other hand, we prove that error explanation based on the second heuristic is tractable for several models that capture program behavior