Name
Abstract | ||
|---|---|---|
Timed behavior automata allow surprisingly efficient model checking of delay-constrained reactive systems when partial-order methods for delay-insensitive systems are adapted for real time. The complexity of timing verification is a sensitive function of the precise abstraction of real time used in the model. Untimed behavior automata [14] are modified in two ways: (i) process output actions are performed inside a timing window relative to the holding of their presets, and (ii) acknowledgment of process input actions is replaced by observing minimum delays between old and new inputs. We prove timing-window bounds on system responses, and show that system inputs do not arrive too fast. Since nonsingleton presets are common, we develop a semantics to reason about nonbinary delay constraints. Model checking starts by coupling specification mirror to implementation network; in timed systems, questions of graph connectivity become questions of constraint graph satisfaction that are computed by optimized linear-time shortest-path algorithms. In the generalized TBA model, nondeterministic input choice is process-scheduled testing of an environment-controlled state predicate; the generalized model, which focuses on mixed-type critical races, is deferred. |
Year | DOI | Venue |
|---|---|---|
1992 | 10.1007/3-540-56496-9_11 | CAV |
Keywords | Field | DocType |
verifying timed behavior automata,nonbinary delay constraints,model checking,graph connectivity,partial order,reactive system,real time,process scheduling,shortest path algorithm,linear time | Model checking,Nondeterministic algorithm,Computer science,Automaton,Constraint graph,Algorithm,Theoretical computer science,Connectivity,Reactive system,Process output,Semantics | Conference |
ISBN | Citations | PageRank |
3-540-56496-9 | 1 | 0.36 |
References | Authors | |
8 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| David K. Probst | 1 | 103 | 29.79 |
| Hon F. Li | 2 | 180 | 51.45 |