Abstract
Conformance testing is the problem of determining if a black-box implementation I is equivalent to a specification S, where both are modeled as finite state Mealy machines. The problem involves constructing a checking sequence based on the specification, which is a sequence of inputs that detects all faulty machines. Traditionally, conformance testing algorithms have assumed that the number of states in the implementation does not exceed that in the specification. This is because it is known that, in the absence of this assumption, the length of the checking sequence needs to be at least exponential in the number of extra states in the implementation. However, this has limited the applicability of these techniques in practice where the implementation typically has many more states than the specification. In this paper we relax the constraints on the size of the implementation and investigate the existence of polynomial length checking sequences for implementations with extra states, under the promise that they either have multiple faults or no faults at all. We present randomized algorithms to construct checking sequences that catch faulty implementations with at most Δ extra states, having at least r faults (where Δ and r are parameters to the algorithm), and pass all correct implementations. We demonstrate the near optimality of our algorithms by presenting lower bounds for this problem. One of the main technical lemmas used in our proof is an estimate of the probability that a random walk on directed graphs will reach a large target set. We believe that this lemma will be of independent interest in the context of verifying safety properties.
Original language | English (US) |
---|---|
Pages | 1136-1145 |
Number of pages | 10 |
State | Published - 2005 |
Event | Sixteenth Annual ACM-SIAM Symposium on Discrete Algorithms - Vancouver, BC, United States Duration: Jan 23 2005 → Jan 25 2005 |
Other
Other | Sixteenth Annual ACM-SIAM Symposium on Discrete Algorithms |
---|---|
Country/Territory | United States |
City | Vancouver, BC |
Period | 1/23/05 → 1/25/05 |
ASJC Scopus subject areas
- Software
- General Mathematics