Name
Abstract | ||
|---|---|---|
Timed behavior automata are finite-state generators of timed behaviors, which are infinite timing-constrained pomsets of system events. Automatic verification is not showing inclusion of infinitary timed string languages. Rather, model checking starts by linking specification mirror and implementation network; verification is showing satisfaction of an infinite timing-constraint graph with recurrence structure. Branching controlled by input/output races models more interesting timing properties such as timeout and exception handling. We show how to mirror timed behavior automata with input/output races, and show that constraint-graph satisfaction can still be computed efficiently by linear-time shortest-path algorithms. The advantage of TBA over timed -automata is ease of mirroring. Untimed behavior automata [14] are modified in two ways: (i) output actions are performed inside a timing window relative to their enabling, and (ii) it is assumed that input actions are performed inside a timing window relative to their enabling. Failure and timeout semantics define the process response to violations of this assumption protocol. |
Year | DOI | Venue |
|---|---|---|
1993 | 10.1007/3-540-56922-7_35 | CAV |
Keywords | Field | DocType |
verifying timed behavior automata,output critical races,input output,model checking,exception handling,shortest path algorithm,linear time | Model checking,Computer science,Automaton,Constraint graph,Exception handling,Algorithm,Input/output,Theoretical computer science,Timed automaton,Timeout,Semantics | Conference |
ISBN | Citations | PageRank |
3-540-56922-7 | 0 | 0.34 |
References | Authors | |
12 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| David K. Probst | 1 | 103 | 29.79 |
| Hon F. Li | 2 | 180 | 51.45 |