Author name cluster

R.P. Kurshan

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

TCS Journal 2004 Journal Article

Minimal length test vectors for multiple-fault detection

Z. Füredi
R.P. Kurshan

A methodology for circuit testing is proposed for detecting multiple circuit faults in the course of a minimal length “guided tour” of the circuit transition structure. Deriving a test vector to guide this tour through an n state subsystem with at most I inputs possible in situ at each state, corresponds to solving an open tour multigraph version of the “Chinese Postman” problem, in which out-degrees are bounded by I. In this case, the length L of a minimal length open tour is shown to satisfy L⩽In 2; a minimal length open tour is computable in O(n 3+nI) steps for undirected multigraphs and O(n 3+(nI)2logn/logI) steps for directed multigraphs, both one-time costs, using weighted matching and bipartite weighted matching, respectively. An open tour can result in a test vector as much as 1 2 shorter than the test vector associated with a closed tour, without any loss in error detection. Examples show that for a directed graph, the length of a minimal length open tour may be as great as n 3/6 for I=n, or Ω(n2) when I is bounded, while in an undirected multigraph, a minimal length tour requires no more than n−3 repeated state transitions. This mitigates in favor of “mixed” circuits in which certain transitions are reversible and need be tested in only one direction. The practicality of this approach rests with the ability to apply it separately to small subsystems, in conjunction with symbolic testing of inter-subsystem coordination. The former is feasible with existing commercial technologies, such as electron beam scanning, while the latter is feasible with a finite-state model-checker. In summary, the proposed methodology comprises three steps: 1. decompose a circuit into subsystems sufficiently small to be model-checked exhaustively; 2. perform symbolic tests of inter-subsystem coordination and conclude that if each subsystem is correctly implemented, then the entire circuit will behave as required; 3. for each circuit subsystem, exercise every realizable transition through a minimal length (open) tour, comparing the actual transitions with those of the specification.

Details DOI

I&C Journal 1995 Journal Article

A Structural Induction Theorem for Processes

R.P. Kurshan
K.L. McMillan

This paper deals with the formal verification of finite state systems that hav an arbitrary number of isomorphic components. We present a technique for inductively generalizing tests on a system of fixed size in order to show that a system of arbitrary size satisfies a given specification. This makes it possible to use finite state verification systems, such as COSPAN, to verify parameterized protocols. The method also may be useful for verifying systems of fixed but large size, since it reduces the size of the system that must be checked automatically. The basis of the method is a structural induction theorem for processes, which is stated and proved in this paper. The theorem applies to a variety of process formalisms satisfying simple algebraic laws. We give examples of proofs using the calculus of communicating systems (CCS) and the s/r model.

Details DOI

I&C Journal 1995 Journal Article

Timing Verification by Successive Approximation

R. Alur
A. Itai
R.P. Kurshan
M. Yannakakis

We present an algorithm for verifying that a model M with timing constraints satisfies a given temporal property T. The model M is given as a parallel composition of ω-automata Pi, where each automaton Pi is constrained by bounds on delays. The property T is given as an ω-automaton as well, and the verification problem is posed as a language inclusion question L (M) ⊆ L (T). In constructing the composition M of the constrained automata Pi, one needs to rule out the behaviors that are inconsistent with the delay bounds, and this step is (provably) computationally expensive. We propose an iterative solution which involves generating successive approximations Mj to M, with containment L (M) ⊆ L (Mj ) and monotone convergence L (Mj ) → L (M) within a bounded number of steps. As the succession progresses, the approximations Mj become more complex. At any step of the iteration one may get a proof or a counter-example to the original language inclusion question. The described algorithm is implemented into the verifier Cospan. We illustrate the benefits of our strategy through some examples.

Details DOI