Compositional LivenessPreserving Conformance Testing of Timed IO Automata IO conformance testing theories (e.g., ioco) are concerned with formally defining when observable output behaviors of an implementation conform to those permitted by a specification. Thereupon, several realtime extensions of ioco, usually called tioco, have been proposed, further taking into account permitted delays between actions. In this paper, we propose an improved version of tioco, called live timed ioco (ltioco), tackling various weaknesses of existing definitions. Here, a reasonable adaptation of quiescence (i.e., observable absence of any outputs) to realtime behaviors has to be done with care: ltioco therefore distinguishes safe outputs being allowed to happen, from live outputs being enforced to happen within a certain time period thus inducing two different facets of quiescence. Furthermore, tioco is frequently defined on Timed IO Labeled Transition Systems (TIOLTS), a semantic model of Timed IO Automata (TIOA) which is infinitely branching and thus infeasible for practical testing tools. Instead, we extend the theory of zone graphs to enable ltioco testing on a finite semantic model of TIOA. Finally, we investigate compositionality of ltioco with respect to parallel composition including a proper treatment of silent transitions.

Relative Liveness: From Intuition to Automated Verification We define a new liveness condition for asynchronous circuits. Although finitary (finiteexecution) descriptions are not powerful enough to express general liveness properties, those liveness properties needed in practice appear to be related in a unique manner to finitary descriptions. Our liveness condition exploits this observation and is defined directly on finitary descriptions, in two forms: one on finite trace structures and the other on finite automata. We prove the equivalence of these two forms. We also introduce a safety condition and derive theorems for the modular and hierarchical verification theorems of both safety and liveness. Finally, we give an algorithm for verifying our liveness condition.