Verifying timed behavior automata with input/output critical races

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.