Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO Laura Brandán Briones2
arXiv:2609.17640v1 [cs.SE] 15 Sep 2026
1
, Petra van den Bos1
, and Marcus Gerhold1
Formal Methods and Tools, University of Twente, The Netherlands {m.gerhold, p.vandenbos}@utwente.nl 2 FaMAF, Universidad Nacional de Córdoba, Argentina [email protected]
Abstract. In Model-Based Testing (MBT), test suites are generated automatically from a formal specification. The theory of testing realtime systems is rich, but often underused in practice, partly because applying the timed machinery demands expertise practitioners should not need. In prior work we addressed this for timed testing with a canonic lifting operator, which lets a modeller specify behaviour as plain labelled transition systems while implicitly obtaining the timed automata that express their quiescent behaviour (the explicit absence of outputs) with timers. This paper takes the next step: we show that our lifting still works when each component carries its own time-out on its own channel. This way, we introduce a multi-channel lifting. We show that it commutes with parallel composition, i.e. composing and lifting is the same as lifting first and then composing. We show that the MBT apparatus survives: conformance, test generation and verdicts are preserved by the lifting, on the testable traces that a time-out based tester can observe. Keywords: Model-based testing · Quiescence · Timed automata · Multichannel systems · Parallel composition · Compositionality.
1
Introduction
Model-based testing (MBT) derives test cases automatically from a behavioural specification model and executes them against a system under test. The input– output conformance relation ioco [19] is the de-facto standard correctness criterion for systems exhibiting nondeterministic behaviour. A distinctive feature of ioco is its explicit treatment of quiescence, i.e. the specified absence of outputs, commonly labelled δ. In practice, testers detect quiescence through a time-out: if no output is observed within some finite time, the system is deemed quiescent. Several timed variants of ioco reflect this, notably tioco [13], rtioco [12] and the quiescence-focused tiocoM [4]. In prior work [6] we showed that these timed models need not be built by hand. Instead, the modeller specifies the system as a plain Labeled Transition System (LTS), and a canonic lifting χM supplies the timing automatically by adding a clock and a global time-out M . This produces a timed automaton and turns quiescence into a real time-out observation,
2
Laura Brandán Briones
, Petra van den Bos
, and Marcus Gerhold
as is commonly done in practice albeit without the formal underpinning. The lifting χM comes with strong guarantees, as it preserves ioco, commutes with test generation, and preserves test verdicts. In short, the modeller keeps working untimed and obtains the entire timed testing machinery for free. This lifting, however, provides a single global time-out, and real systems rarely admit only one. To illustrate, suppose two components have been specified independently, each with its own natural time-out M1 and M2 , and suppose M1 ≪ M2 . Running the composed system under the single-M lifting of [6] forces a choice. Taking M = min(M1 , M2 ) declares the slower channel quiescent prematurely and so accepts implementations the specification rejects. Taking M = max(M1 , M2 ) is sound but pointless, since every quiescence verdict on the faster channel is delayed until the slower channel’s deadline. This inflates test-execution time needlessly. Even worse, any single intermediate M inherits both downsides and collapses the two components’ quiescence labels δ1 , δ2 into a single δ, so the tester loses the ability to even tell which channel has gone silent. This motivates our current work: a multi-channel refinement of the lifting. It combines two existing pieces of work. The first is untimed multi-channel ioco [3,10], where outputs are partitioned into channels, each with its own quiescence, yielding the relation m-ioco. The second is its timed multi-channel counterpart m-tiocoM of Brandán Briones and Brinksma [5], which equips each channel with its own time-out. Our paper provides the bridge between them: a canonic lifting that lets the modeller continue to work on an untimed model and obtain the multi-channel timed theory for free. Moreover, this lifting is compositional, meaning lifting the parallel composition of several components equals the parallel composition of the lifted components. A modeller can therefore build and time each component independently. Contributions. Concretely, our contributions are as follows. ◦ We introduce the multi-channel canonic lifting χM , which augments a labelled transition system with one clock and one quiescence time-out per output channel (Section 5), generalising the single-time-out lifting of [6]; ◦ We show that χM bridges untimed multi-channel ioco with the timed one m-tiocoM (Theorem 1): AI m-iocoM AS iff χM (AI ) m-tiocoM χM (AS ); ◦ We show that χM commutes with test-case generation and preserves test verdicts (Section 6); ◦ We prove that χM commutes with (shared-environment) parallel composition (Theorem 4), i.e. χM1 ⌢M2 (A1 ∥ A2 ) = χM1 (A1 ) ∥ χM2 (A2 ). The extension is not a trivial generalisation of [6], since per-channel bounds may order quiescence observations in a suspension trace in a way no time-out based tester can produce in practice. To address the correspondence between the untimed and timed theories we define testable traces (Definition 13). Paper overview. Section 2 recalls labelled transition systems, and Section 3 fixes a multi-channel version of ioco along the lines of [3]. Section 4 recalls timed automata and the timed multi-channel relation m-tiocoM along the lines of [5].
Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO
3
Section 5 defines the lifting χM and proves the conformance bridge. Section 6 treats test generation and commutation. Section 7 develops the compositionality theorem and the corresponding conformance corollary. Sections 8 and 9 discuss related work and conclude. This technical report includes proofs in Appendix A.
2
Labelled Transition Systems
Labelled transition systems have transitions labelled with actions. We fix a finite set of input actions Act I and a finite set of output actions Act O and write Act = Act I ∪ Act O . Inputs are suffixed with ?, outputs with !, which are conventions on the naming of labels, not part of the labels themselves. In LTSs, τ is often used to mark internal and invisible progress. For the sake of simplicity, we exclude τ -actions for now, though including it is not expected to cause any issues [7]. Definition 1 (Labelled transition system). A labelled transition system (LTS) is a tuple A = ⟨S, Act, →, s0 ⟩, where S is a finite set of states with unique initial state s0 ∈ S and →⊆ S × Act × S is the transition relation. a
a
a
– We write s − → s′ for (s, a, s′ ) ∈→, and s − → if s − → s′ for some s′ ∈ S and a ′ s− → ̸ if no such s exists; σ – For σ = a1 · · · an with ai ∈ Act, we write s − → s′ if there exist states a i s0 , s1 , . . . , sn with s0 = s, sn = s′ , and si−1 −→ si for all 1 ≤ i ≤ n; ∗ we call σ ∈ Act a trace; σ – We write traces(s) = {σ ∈ Act ∗ | s − →} and set traces(A) = traces(s0 ). In ioco theory the implementation model is assumed to be input-enabled. The intuition is that a tester is always able to provide any input to the system at any given time. In our paper we make this distinction explicit by calling input-enabled systems input-output transition systems (IOTSs). Definition 2 (IOTS). An input-output transition system (IOTS) is an LTS i?
A = ⟨S, Act, →⟩ that is input-enabled, i.e.: ∀ s ∈ S : ∀ i? ∈ Act I : s −→ .
3
Multi-channel ioco
Following [3], we partition the output alphabet into a fixed number of channels. We will see later that each channel represents a component in a composed system. Definition 3 (Output channels). Let n ≥ 1 for U an n ∈ N. An n-channel n output partition is a family {Act kO }nk=1 with Act O = k=1 Act kO , i.e. the channels cover Act O and are pairwise disjoint. We write Act k = Act I ∪ Act kO . The channel of an output o! ∈ Act O is the unique k with o! ∈ Act kO . While Heerink [10] partitions both inputs and outputs into channels, we partition only outputs and keep inputs as a single shared set. This reflects the intuition that quiescence is an output observation: the tester controls when inputs are provided, but only observes when outputs are (resp. are not) emitted. Consequently, we later assume that inputs are shared among all components.
4
Laura Brandán Briones
, Petra van den Bos
, and Marcus Gerhold
Definition 4 (Per-channel quiescence). Let A be an LTS with an n-channel output partition. A state s ∈ S is k-quiescent if there is no outgoing output o! transition in Act kO from s, i.e. ∀ o! ∈ Act kO : s − ̸ →. We introduce a fresh channelindexed quiescence action δk for each channel k ∈ {1, . . . , n} and write Act δO = Act O ∪ {δ1 , . . . , δn },
Act δ = Act ∪ {δ1 , . . . , δn }.
Naturally, a state is quiescent in the classical sense [19] iff it is k-quiescent for every k. We augment traces to include the k-quiescence labels (δ1 , . . . , δk ) and call the resulting set suspension traces. We follow our previous work [6] closely to introduce more notation needed for multi-channel ioco. Definition 5 (Multi-channel ioco notation). Let A = ⟨S, Act, →, s0 ⟩ be an LTS with an n-channel output partition, and s ∈ S. Then: – The channel-k outputs of s are o!
→} ∪ {δk | s is k-quiescent} out k (s) = {o! ∈ Act kO | s − – Given the empty sequence ε, a ∈ Act δ and σ ∈ (Act δ )∗ the states-after-trace relation, extended from single actions a to sequences σ, is: s after ε = {s} a
s after a = {s′ ∈ S | a ∈ Act, s − → s′ } ∪ {s | a = δk , s is k-quiescent} [ s after a σ = {s′ after σ | s′ ∈ s after a} – The suspension traces (i.e. traces explicitly including the δk labels) of s are Straces(s) = {σ ∈ (Act δ )∗ | s after σ ̸= ∅}, and Straces(A) = Straces(s0 ). This enables us to define multi-channel ioco where the intuition is straightforward: rather than having one output channel there are multiple. Note that, unlike out k the operator after is channel-agnostic. Definition 6 (Multi-channel ioco). Let AS be an LTS and AI an IOTS over the same set of inputs Act I and the same n-channel output partition. Then AI m-ioco AS iff ∀ σ ∈ Straces(AS ) : ∀ k ∈ {1, . . . , n} : out k (AI after σ) ⊆ out k (AS after σ). Definition 6 collapses to classical ioco of [19] when n = 1, i.e. there is a single output channel and a single quiescence action δ = δ1 . The channel partition originates from [3] and was later refined in [10]; the per-channel quiescence labels δk were later added in the timed setting of [5]. Therefore, Definition 6 can be considered the untimed restriction of the relation m-tiocoM of [5]. Example 1 (Display component). Figure 1 shows the UI component AUI of an ATM, a single-channel LTS with inputs Act I = {card ?, pin?} and outputs Act 1O = {msg!, err !} holding status messages and error reports. It is an LTS but not an IOTS, since neither of the states accepts all inputs. Figure 1(b) adds the per-channel quiescence loops, i.e. s0 and s2 are 1-quiescent and have a δ1 loop, whereas s1 and s3 have an enabled output and no δ1 -loop. In Section 7 we compose AUI with a cash dispenser to obtain a two-channel system.
Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO
5
δ1 s0 msg!
card ?
err ! s3
pin?
s1 msg!
s0 msg!
s2
(a) AUI as an LTS.
card ?
msg!
err ! s3
s1
pin?
s2
δ1
(b) AUI with 1-quiescence.
Fig. 1: The LTS AUI over the single channel Act 1O = {msg!, err !}. Figure (a) is the plain LTS. Figure (b) adds the δ1 self-loops at the 1-quiescent states s0 and s2 . States s1 and s3 are not 1-quiescent since msg! (err! resp.) is enabled.
4
Timed Automata and Multi-Channel m-tiocoM
We assume that the reader is familiar with timed automata following Alur [1] and only briefly recall what we need here. Let C be a finite set of clocks and Φ(C) the set of clock constraints generated by the grammar: φ ::= c ∼ K | φ1 ∧ φ2 for c ∈ C, K ∈ R≥0 , ∼ ∈ {<, ≤, =, ≥, >}. As per usual, a clock valuation v : C → R≥0 assigns each clock its current value. Definition 7 (Timed automaton). A timed automaton (TA) is a tuple A = ⟨L, Act, ΦL , C, →, ℓ0 ⟩ where L is a finite set of locations with initial location ℓ0 ∈ L, ΦL : L → Φ(C) assigns an invariant to each location, and →⊆ L × Act × Φ(C) × 2C × L is the transition relation. A transition ⟨ℓ, a, φ, λ, ℓ′ ⟩ is enabled when its guard φ holds; when a transition is taken the clocks in λ reset to zero. We exclude Zeno behaviour, i.e. infinite transitions in a finite amount of time. (d,a)
– We write ℓ −−−→ ℓ′ for (d, a) ∈ R≥0 × Act if there is ⟨ℓ, a, ϕ, λ, ℓ′ ⟩ ∈ − → such that ϕ and Φ(ℓ) are true for time d that is spent between ℓ and ℓ′ , and such that Φ(ℓ′ ) is true after updating the clocks with the resets from λ; – We lift → − to sequences, i.e. for ρ = (d1 , a1 ) · · · (dn , an ) ∈ (R≥0 × Act)∗ , ρ we write ℓ − → ℓ′ if there are locations ℓ0 , . . . , ℓn with ℓ0 = ℓ, ℓn = ℓ′ , and (di ,ai )
ρ
ρ
ℓi−1 −−−−→ ℓi for all 1 ≤ i ≤ n. As before, ℓ − → means ℓ − → ℓ′ for some ℓ′ ; – Timed traces are sequences of non-negative numbers and visible actions, i.e. ρ ttraces(ℓ) = {ρ ∈ (R≥0 × Act)∗ | ℓ − →}. Like before, we require an implementation to be input-enabled. For a TA, a location ℓ is input-enabled if every input is enabled from ℓ at any d, i.e. ∀ i? ∈ (d,i?)
Act I : ℓ −−−→. An input-output timed automaton (IOTA) requires this while every channel is still below its quiescence bound. To formally quantify quiescence
6
Laura Brandán Briones
, Petra van den Bos
, and Marcus Gerhold
and anchor it in real-time we fix a vector M = [M1 , . . . , Mn ] ∈ Rn>0 . These Mk later serve as per-channel quiescence bounds. Definition 8 (IOTA). TA A is an input-output timed automaton (IOTA) for M = [M1 , . . . , Mn ] ∈ Rn>0 if every location ℓ ∈ L is input-enabled under (d,i?)
every time d: ∀ i? ∈ Act I : ∀ ℓ ∈ L : ∀ d ∈ R≥0 : d < Mk : ℓ −−−→. The strict inequality d < Mk for all channels k is deliberate, i.e. once a channel has reached its bound it has to conclude quiescence. Since this changes the suspension context, input-enabledness is required only before that point. We now lift the abstract notion of per-channel quiescence from the untimed setting to TAs. Unlike input-enabledness, k-quiescence checks the absence of k-channel output transitions enabled at ℓ. Definition 9 (k-quiescent). Let A be a TA with output partition {Act kO }nk=1 and bounds M = [M1 , . . . , Mn ] ∈ Rn>0 . A location ℓ ∈ L is k-quiescent if: (d,o!)
̸ −→ . ∀ d ∈ R≥0 : d < Mk : ∀ o! ∈ Act kO : ℓ −− Unlike input-enabledness, k-quiescence checks the absence of k-channel output transitions enabled at ℓ, which no clock valuation can affect. We therefore state it via a delay d rather than a valuation. Below we introduce some notations that are needed to define m-tiocoM . Definition 10 (m-tiocoM notation). We define: – For each channel k: (d,o!)
k out M k (ℓ) ={(d, o!) ∈ (R≥0 ×Act O ) | ℓ −−−→}∪
{(d, δk ) | ℓ is k-quiescent ∧ d = Mk } – As in Definition 5 we extend (and overload) after as follows: ℓ after ϵ ={ℓ} (d,a)
ℓ after (d , a) ={ℓ′ | a ∈ Act ∧ ℓ −−−→ ℓ′ } ∪ {ℓ | (d , a) = (Mk , δk ) ∧ ℓ is k-quiescent} [ ℓ after (d , a)ρ = {ℓ′ after ρ | ℓ′ ∈ ℓ after (d , a)} – We define the suspension timed traces as the traces of location ℓ, including δk at time Mk , for k-quiescent locations encountered in the timed trace: SttracesM (ℓ) = {ρ ∈ (R≥0 × Act δ )∗ | ℓ after ρ ̸= ∅}. – We write: A after ρ = ℓ0 after ρ and SttracesM (A) = SttracesM (ℓ0 ). We can now define the timed, multi-channel conformance relation m-tiocoM .
Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO
7
Definition 11 (m-tiocoM ). Let AS be a TA and AI an IOTA over the same output partition {Act kO }nk=1 with M = [M1 , . . . , Mn ]. Then, AI m-tiocoM AS M iff ∀ ρ ∈ SttracesM (AS )∀ k ∈ {1, . . . , n} : out M k (AI afterρ) ⊆ out k (AS afterρ). Definition 11 matches the relation introduced in [5] in spirit, up to cosmetic changes that align the notation with our previous paper [6]. As in the untimed case, and contrary to [5], we assume a single shared input channel.
5
The Canonic Multi-Channel Lifting χM
We now define the lifting operator χM in Definition 12 as multi-channel counterpart of our previous work in [6], with one clock per channel, as first outlined in [4]. The full TA formalism (cf. [1]) admits intricate constructions that we do not need. The lifting produces only a restricted, canonic TA V that has exactly one clock per V output channel, location invariants of the shape k ck ≤ Mk , guards of the form k ck < Mk (inputs), ck < Mk (k-outputs) or ck = Mk (k-quiescence), and resets of the form {ck } (k-outputs or k-quiescence) or C (all clocks, for inputs). An output on channel k resets only ck , since it is no evidence of activity on any other channel k ′ ̸= k. Inputs, by contrast, reset all clocks. Since an input is global tester activity, once the tester provides a stimulus, quiescence is measured freshly on every channel and all their timers are reset. The invariant forces each channel to conclude quiescence at exactly its own bound, i.e. once ck reaches Mk , no further time may elapse until δk is observed. We represent χM graphically in Table 1. Corollary 1 states that IOTS map to IOTA, as expected. Definition 12 (Multi-channel lifting χM ). Let A = ⟨S, Act, →, s0 ⟩ be an LTS with n-channel output partition {Act kO }nk=1 , and M = [M1 , . . . , Mn ] ∈ Rn>0 . The canonic multi-channel TA of A is the result of the mapping χM : LTS → TA such that χM (A) = ⟨L, Act δ , ΦL , C, →A , ℓ0 ⟩ where – L = S, with ℓ0 = s0 ; – C = {c1 , .V . . , cn }, one clock per output channel; n – ΦL (ℓ) = ( k=1 ck ≤ Mk ), the location invariants; – →A : L × Act × Φ(C) × 2C × L defines transition relation →A as an extension of → with clock Vnconstraints and resets, as follows: →A = {(ℓ, a, k=1 ck < Mk , C, ℓ′ ) | (ℓ, a, ℓ′ ) ∈ →, a ∈ Act I } ∪ {(ℓ, a, ck < Mk , {ck }, ℓ′ ) | (ℓ, a, ℓ′ ) ∈ →, a ∈ Act O } ∪ {(ℓ, δk , ck = Mk , {ck }, ℓ) | ℓ ∈ L is k-quiescent}. Corollary 1 (Input-enabledness under χM ). χM maps IOTSs to IOTAs. Example 2 (Lifting the UI). We apply χM to Aui with the single bound M1 = 1, indicating that the user interface must conclude quiescence within one time unit. Figure 2 shows the result. Clock c1 tracks UI quiescence and every location carries the invariant c1 ≤ 1. Each output (msg!, err !) is guarded by c1 < 1 and
8
Laura Brandán Briones
, Petra van den Bos
, and Marcus Gerhold
Table 1: Representation of χM (cf. Definition 12) with n = 2 channels. Inputs reset all clocks; an output on channel k resets only ck ; each k-quiescent location adds a quiescence self-loop δk with guard Mk , independently of the other channel. Input i? LTS
TA after χM
Output ch. k ok ! ok !
i? i? c1 ≤ M1 c1 < M1 ∧ c2 < M2 ∧ {c1 , c2 } c2 ≤ M2
δ1 , c1 = 1, {c1 }
s0
c1 ≤ M1 ∧ c2 ≤ M2
card? c1 < 1, {c1 }
c1 ≤1
msg! c1 < 1, {c1 }
δk c1 ≤ M1 ∧ c2 ≤ M2
{ck }
δk ck = M k {ck }
s1 c1 ≤1
err ! c1 < 1, {c1 }
s3 c1 ≤1
ok ! c k < Mk
Quiescence δk
msg! c1 < 1, {c1 }
s2 pin? c1 < 1, {c1 }
c1 ≤1
δ1 , c1 = 1, {c1 }
Fig. 2: The lifted UI component χ[1] (AUI ) with bound M1 = 1. Every location carries the invariant c1 ≤ 1. Outputs are guarded c1 < 1 and reset c1 ; the δ1 loops are enabled at c1 = 1 at the UI-quiescent locations s0 and s2 .
resets c1 , while the δ1 self-loops at s0 and s2 are enabled at exactly c1 = 1 and reset c1 . Inputs reset c1 as well indicating that the tester provided a stimulus. This is the single-channel construction of our prior work [6]; the multi-channel structure is shown once we compose in Section 7.
Preservation of Conformance. The core of our work is that the untimed m-ioco relation (cf. Definition 6) matches the timed multi-channel relation (cf. Definition 11) after lifting. In other words, the lifting preserves conformance. To formally prove that, we need a language-theoretic result that both systems (before and after the lifting) share the same traces up to timing information. Intuitively, χM makes outputs timed, but does not change which ones are enabled in a state, i.e. a channel-k output at a state becomes the timed observations {(d, o!) : d < Mk }, and k-quiescence becomes the single observation (Mk , δk ). Untimed and timed observations thus correspond per channel. In particular, for a timed trace ρ, its projection ρ↓ removes all delays, i.e. for the empty sequence ε it is ε↓ = ε and otherwise inductively ((d, a)·ρ′ )↓ = a·(ρ′ ↓). Intuitively, ρ↓ = σ means ρ and σ agree on actions and ignore timing (Lemma 1). Lemma 1 (Multi-channel canonic traces). Let A = ⟨S, Act, →, s0 ⟩ be an LTS with an n-channel output partition and M = [M1 , . . . , Mn ] ∈ Rn>0 , then: If ρ ∈ SttracesM (χM (A)), then there is σ ∈ Straces(A) such that ρ↓ = σ.
Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO
9
In the other direction, we need to be more careful. An LTS may have some traces, that are not testable after lifting to the timed setting. Consider a trace δ2 o1 for M1 < M2 : it models that output o1 from channel 1, that should only be allowed before time-out M1 , could happen after time-out M2 (due to the preceding δ2 ), which contradicts that output o1 is allowed (before M1 < M2 ). The lifted TA excludes this behaviour by making bounds explicit. Definition 13 restricts suspension traces to only the testable traces. Concretely, a suspension trace is testable iff its quiescence observations respect the ordering of the bounds and no δk occurs while a faster channel k ′ (Mk′ < Mk ) has been silent for at least Mk′ without δk′ being observed. The trace δ2 o1 above violates this and describes an observer who has skipped a timeout that necessarily happened but was not observed by any timeout-based tester. Definition 13 (Testable traces). Let A be an LTS with an n-channel output partition and M = [M1 , . . . , Mn ] ∈ Rn>0 . The set of testables traces are: TStraces(A) = {σ ∈ Straces(A) | ∃ρ ∈ SttracesM (χM (A)) : ρ↓ = σ}. Definition 13 identifies the suspension traces that survive the lifting. Restricting m-ioco to these traces yields a relation that, by Lemma 1, matches m-tiocoM exactly. Definition 14 introduces the restricted relation m-iocoM , using outputs out T , that only omits a δk from out that no realization of σ can observe, i.e. when σ is not a testable trace. Definition 14 (Testable multi-ioco). For an LTS A, σ ∈ Straces(A) and channel k, let out Tk (A, σ) = {a ∈ Act kO ∪ {δk } | σ · a ∈ TStraces(A)}. Then AI m-iocoM AS iff ∀σ ∈ TStraces(AS ) ∀k : out Tk (AI , σ) ⊆ out Tk (AS , σ). Theorem 1 (Preservation). Let AI be an IOTS and AS an LTS over the same n-channel output partition. For every M = [M1 , . . . , Mn ] ∈ Rn>0 : AI m-iocoM AS if and only if χM (AI ) m-tiocoM χM (AS ).
6
Test Cases and Commutation
We define multi-channel test cases for LTSs and TAs, respectively. Similar to our previous work [6] test cases are inspired from the literature [19,23]. We further connect these test cases to conformance by showing that verdicts are preserved by the lifting. An implementation passes every untimed test case iff its lifting passes every timed test case. As usual in ioco-theory, the tester’s choices at each state (resp. location) are: (1) stop; (2) observe outputs or quiescence; or (3) stimulate with an input. Our test cases here range over the augmented alphabet Act δ = Act ∪ {δ1 , . . . , δn }; the multi-channel aspect is precisely that quiescence is observed per channel, via the labels δ1 , . . . , δn , rather than through a single δ.
10
Laura Brandán Briones
, Petra van den Bos
, and Marcus Gerhold
Definition 15 (Multi-channel LTS test case). A test for an LTS AS with n-channel output partition and bounds M is a tree-shaped LTS t = ⟨S t , Act δ , →t , st0 ⟩ satisfying: – t uses the same action labels and partitioning as AS plus δ1 , . . . , δn ; – t has only finite traces, is deterministic, and has no cycles; – There are two special states pass, fail ∈ S t ; – States pass and fail have no outgoing transitions; – Every other state except pass and fail enables all outputs Act O , and either one input or all δk , i.e. ∀ s ∈ S t \ {pass, fail} : (|in(s)| = 0 ∧ out(s) = Act O ∪ {δ1 , . . . , δn }) ∨ (out(s) = Act O ∧ |in(s)| = 1); – Input-specifiedness: All traces of t that end with an input are testable traces of AS , i.e. ∀ σ ∈ traces(t), ∀ i? ∈ Act I : σ · i? ∈ traces(t) ⇒ σ · i? ∈ TStraces(AS ); – Soundness: All traces of t leading to pass are testable traces of AS : σ ∀ σ ∈ traces(t) : t − → pass ⇒ σ ∈ TStraces(AS ); – Correctness: All traces of t that end with an output or any δk , and lead to fail, are not testable traces of AS : σ·o ∀ σ ∈ traces(t), ∀ o ∈ Act O ∪ {δ1 , . . . , δn } : σ · o ∈ traces(t) ∧ t −−→ fail ⇒ σ·o∈ / TStraces(AS ). Test cases thus depend on M through TStraces. Note that correctness also uses TStraces, i.e. a trace that is not testable cannot be observed by a timeout based tester. A natural refinement in the multi-channel setting would allow “per-channel observe states”, i.e. states enabling Act O ∪ {δk } for a single channel k. Operationally this lets a test focus on one channel (e.g. waiting out the cash channel’s time-out without branching on display-channel observations it does not care about), which can yield smaller, more targeted tests. The trade-off is that ignoring one channel shifts the burden of detecting the other channels’ faults onto other tests. Hence, coverage must be recovered across the test suite rather than within each test. As in [6] test verdicts are defined on traces alone; we do not parallel-compose tests with implementations. The parallel composition we use here (cf. Definition 17) composes system specifications, not implementation models and tests as sometimes done in ioco literature [18]. Here, verdicts are defined in a lightweight way: AI fails t iff some trace σ ∈ TStraces(AI )∩traces(t) leads to fail, and passes otherwise. We lift this to a set of tests (a test suite) T and say AI passes T iff it passes every t ∈ T , and fails T iff it fails some t ∈ T . Definition 16 (Multi-channel TA test case). A timed test case for a canonic TA A = χM (AS ) with an n-channel output partition is a tree-shaped TA tTA = ⟨LtTA , Act δ , ΦtLTA , C, →tTA , ℓt0TA ⟩ satisfying: – tTA uses the same action labels and partitioning as AS plus δ1 , . . . , δn ; – tTA has timed traces using a finite number of actions, and has no cycles; – every transition of tTA is reachable, i.e. it occurs in some timed trace ρ ∈ ttraces(tTA );
Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO
11
– There are two special locations pass, fail ∈ LtTA ; – Locations pass and fail have no outgoing transitions, – tTA uses the clock set C = {c1 , . . . , cn }, one perVoutput channel. Every nonterminal location carries the canonic invariant k ck ≤ Mk ; – Every non-terminal location enables all outputs Act O and either one input or all per-channel quiescence labels δ1 , . . . , δn , refined per channel as follows: • Each δk -transition carries guard ck = V Mk and reset {ck }; • Each input transition carries guard k ck < Mk and reset C; • Each channel-k output transition carries guard ck < Mk and reset {ck }; – Input-specifiedness: All timed traces of tTA that end with an input are suspension timed traces of A, i.e. ∀ ρ ∈ ttraces(tTA ) ∀ d ∈ R≥0 ∀ i? ∈ Act I : ρ · (d , i?) ∈ ttraces(tTA ) ⇒ ρ · (d , i?) ∈ SttracesM (A); – Soundness: All timed traces of tTA leading to pass are suspension timed traces ρ of A: ∀ ρ ∈ ttraces(tTA ) : tTA − → pass ⇒ ρ ∈ SttracesM (A); – Correctness: All timed traces of tTA that end with an output or δk , and lead to fail are not suspension timed traces of A: ∀ ρ ∈ ttraces(tTA ) ∀ d ∈ R≥0 ∀ o ∈ Act O ∪ {δ1 , . . . , δn } : ρ·(d,o)
ρ · (d , o) ∈ ttraces(tTA ) ∧ tTA −−−−→ fail ⇒ ρ · (d , o) ∈ / SttracesM (A). With test cases defined on both sides of the lifting, the two natural properties to investigate are (1) commutativity of the lifting operator (i.e. whether lifted test cases for the LTS are the same as test cases for the lifted LTS), and (2) the verdict preservation under the lifting. Applied to a test case, χM decorates the existing transitions, including the δk -transitions already present, and adds no self-loops, so pass and fail stay terminal. Strictly, this is another operator; for the sake of brevity we do not spell it out explicitly here. Theorem 2 (Test correspondence). Let TLTS (AS ) be the set of test cases for an LTS AS (Definition 15) and TTA (χM (AS )) the set of timed test cases for χM (AS ) (Definition 16). Then: χM (TLTS (AS )) = TTA (χM (AS )). Theorem 2 shows that the lifting is commutative with respect to test generation, but it does not yet say anything about what running those tests means. The next theorem closes that gap. That is, passing or failing a test in the untimed paradigm agrees with passing or failing the lifted test in the timed paradigm. Theorem 3 (Verdict preservation). every M = (M1 , . . . , Mn ) ∈ Rn>0 :
For every IOTS AI and LTS AS and
1. If AI passes TLTS (AS ), then χM (AI ) passes TTA (χM (AS )). 2. If AI fails TLTS (AS ), then χM (AI ) fails TTA (χM (AS )). Theorems 2 and 3 prove the testing-side of the lifting, i.e. the modeller may continue to construct test cases for the untimed specification, and the verdicts agree with those of the lifted timed tests against the lifted implementation.
12
7
Laura Brandán Briones
, Petra van den Bos
, and Marcus Gerhold
Compositionality
The central result of this section is that the multi-channel lifting χM commutes with parallel composition. Up to clock renaming, lifting a composed specification yields exactly the composition of the lifted specifications of components. This means a practitioner can model each component with its own per-channel timeouts and compose them for testing without losing conformance. We compose components that operate in a shared environment, i.e. each component reacts to the same (external) inputs, while producing outputs on its own disjoint channels. Our composition therefore synchronises components on shared inputs and interleaves every other action. Specifically, we assume that no output of one serves as an input to another as is commonly done in the paradigm of Lynch and Tuttle [15]. Their’s is a richer setting that would interact subtly with quiescence here, since a blocked synchronised output can make a composed state quiescent where a single component is not. Definition 17 (Shared-environment parallel composition of LTSs). Let Ai = ⟨Si , Act i , →i , s0,i ⟩ be LTSs for i = 1, 2 with disjoint output alphabets Act O,1 ∩ Act O,2 = ∅ and shared inputs Act sync = Act I,1 = Act I,2 . Their parallel I composition A1 ∥ A2 consists of the set of states S1 ×S2 , initial state (s0,1 , s0,2 ), and transitions a
if a ∈ Act sync , s1 − → s′1 , s2 − → s′2 ; I
(s1 , s2 ) − → (s′1 , s2 )
a
if a ∈ Act O,1 , s1 − → s′1 ;
a
if a ∈ Act O,2 , s2 − → s′2 .
(s1 , s2 ) − → (s′1 , s′2 ) (s1 , s2 ) − → (s1 , s′2 )
a
a
a
a
Its output partition is the disjoint union of the components’ partitions, so each channel retains its own identity and bound. In the same vein we adapt parallel composition of TAs [1], which adds disjoint clock sets and component-wise joined invariants. Additionally, synchronisation on shared actions joins guards and unifies resets. Given M1 = [M1 , . . . , Mn1 ] ∈ 1 2 Rn>0 and M2 = [M1′ , . . . , Mn′ 2 ] ∈ Rn>0 , we write 1 +n2 M1 ⌢ M2 = [M1 , . . . , Mn1 , M1′ , . . . , Mn′ 2 ] ∈ Rn>0 .
Definition 18 (Shared-environment parallel composition of TAs). Let Ai = ⟨Li , Act i , ΦLi , Ci , →i , ℓ0,i ⟩ be canonic TAs for i = 1, 2 with disjoint clock sets, and output sets Act O,1 ∩ Act O,2 = ∅, and shared inputs Act sync = Act I,1 = I Act I,2 . Then A1 ∥ A2 has location set L1 × L2 , clock set C1 ∪ C2 , initial location (ℓ0,1 , ℓ0,2 ), invariants ΦL1 (ℓ1 ) ∧ ΦL2 (ℓ2 ) for (ℓ1 , ℓ2 ) ∈ L1 × L2 , and transitions: – synchronised, for a ∈ Act sync : ⟨(ℓ1 , ℓ2 ), a, φ1 ∧ φ2 , λ1 ∪ λ2 , (ℓ′1 , ℓ′2 )⟩ whenever I ′ ⟨ℓi , a, φi , λi , ℓi ⟩ ∈ →i ; 1 – interleaved,∀a ∈ Act δO,1 : ⟨(ℓ1 , ℓ2 ), a, φ1 , λ1 , (ℓ′1 , ℓ2 )⟩ when ⟨ℓ1 , a, φ1 , λ1 , ℓ′1 ⟩ ∈ →1 ; 2 – interleaved,∀a ∈ Act δO,2 :⟨(ℓ1 , ℓ2 ), a, φ2 , λ2 , (ℓ1 , ℓ′2 )⟩ when ⟨ℓ2 , a, φ2 , λ2 , ℓ′2 ⟩ ∈ →2 .
Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO δ2
13
δ2 card ?
e0
pin?
e1
e2
money! (a) The cash dispenser Adisp as an LTS s0 , e0 c1 ≤1 ∧c2 ≤5
δ1 ,c1 =1,{c1 } δ2 ,c2 =5,{c2 }
card?
s0 , e0
c1 <1∧c2 <5 {c1 ,c2 }
s1 , e1
card?
c1 ≤1 ∧c2 ≤5 δ2 ,c2 =5,
money! c2 <5,{c2 }
s1 , e1
msg!/err ! c1 <1,{c1 }
{c2 }
msg! c1 <1,{c1 }
money!
msg!/err !
s1 , e2
msg!
δ1 ,c1 =1,
s1 , e2
{c1 }
c1 ≤1 ∧c2 ≤5 δ1 ,c1 =1,{c1 } pin? δ2 ,c2 =5,{c2 } c1 <1∧c2 <5
δ2 ,c2 =5, {c2 }
{c1 ,c2 }
pin?
s2 , e0 c1 ≤1 ∧c2 ≤5
s2 , e 0
msg!/err !
s2 , e3
money!
s0 , e3
(b) AUI ∥ Adisp as an LTS
msg!/err ! c1 <1 {c1 }
s2 , e3 c1 ≤1 ∧c2 ≤5
money! c2 <5 {c2 }
s0 , e3 c1 ≤1 ∧c2 ≤5
(c) TA χ[1] (AUI ) ∥ χ[5] (Adisp ), lifted and composed with M = [1, 5]
Fig. 3: Parallel composition of UI and dispenser (the display Aui is shown in Figure 1. (a) the cash dispenser Adisp ; (b) the LTS composition over states (si , ej ); (c) its lifting with one clock per sub-component, i.e. M = [1, 5].
Example 3 (Composing dispenser and display). The full ATM arises by composing Aui with a cash dispenser Adisp , a single-channel LTS over Act 2O = {money!} that accepts card ? then pin? before dispensing, see Figure 3(a). Figure 3(b) and (c) show the composition before and after the lifting. The components synchronise on the shared inputs card ?, pin? and have disjoint output channels with bounds M1 ⌢ M2 = [1, 5]. In other words, the UI component concludes quiescence in one time unit whereas the dispenser in takes five. The composed state (s2 , e3 ) has no quiescence loop, as both channels have an output enabled, whereas (s0 , e0 ) and (s1 , e2 ) are quiescent on both channels and carry δ1 and δ2 enabled at the different times. Parallel composition of multiple components is one of the main reasons for per-channel time-outs. A single global M like in our previous work [6] forces every component to “share” one quiescence deadline, so a fast component cannot conclude quiescence until the slowest one would. This increases the overall testing time. Per-channel clocks avoid this, because each channel concludes quiescence
14
Laura Brandán Briones
, Petra van den Bos
, and Marcus Gerhold
at its own bound. This keeps verdicts specific and avoids the time overhead of waiting out the slowest channel everywhere. We show that this structure survives composition, since the multi-channel lifting commutes with parallel composition. Theorem 4 (Compositionality). Let A1 , A2 be LTSs with disjoint output 2 1 . Then , M2 ∈ Rn>0 alphabets and shared inputs, and let M1 ∈ Rn>0 χM1 ⌢M2 (A1 ∥ A2 ) = χM1 (A1 ) ∥ χM2 (A2 ). In other words, lifting a composed model gives exactly the composition of the lifted models (up to clock renaming). Thus, a modeller can specify each component in the untimed paradigm with its own bounds and compose the results without ever reasoning about a global time-out or building the multi-channel timed model by hand. With our definition of parallel composition and with the following lemma the conformance under composition then follows immediately. Lemma 2 (Compositionality of testable multi-ioco). Let A1I , A1S and let A2I , A2S be the implementation–specification pairs of LTSs, with A1I , A2I IOTSs. Assume they have disjoint outputs (Act O,1 ∩ Act O,2 = ∅) and shared inputs, 1 2 and have bound vectors M1 ∈ Rn>0 and M2 ∈ Rn>0 . If A1I m-iocoM1 A1S and A2I m-iocoM2 A2S , then A1I ∥ A2I m-iocoM1 ⌢M2 A1S ∥ A2S . Corollary 2 (Composition of timed conformance). Let A1I , A1S and A2I , A2S be implementation–specification pairs of LTSs, with A1I , A2I IOTSs. Assume the pairs have disjoint outputs (Act O,1 ∩ Act O,2 = ∅) and shared inputs, and have 1 2 bound vectors M1 ∈ Rn>0 , M2 ∈ Rn>0 . If A1I m-iocoM1 A1S and A2I m-iocoM2 1 2 M1 ⌢M2 (AI ∥ A2I ) m-tiocoM1 ⌢M2 χM1 ⌢M2 (A1S ∥ A2S ). AS , then χ
8
Related Work
Our contribution sits at the intersection of several extensions of ioco: quiescence, timed conformance, multiple channels, and compositionality. Most prominently, we extend our own prior work [6,7] to a multi-channel setting. Input-Output conformance and quiescence. Our work builds on the ioco testing theory of Tretmans [19]. Stokkink et al. later make quiescence a firstclass citizen through quiescent transition systems [16] and later yet treat divergence explicitly [17]. In [20], Tretmans and Janssen revisit the foundations of the relation and note some shortcomings. Multiple-channels. Heerink [10] introduces refusal testing with multiple input/output channels, and Brandán Briones and Brinksma [5] give a multiinput/output relation; the first is untimed and operates on several input channels, the latter operates on timed-labelled transition systems. Timed testing. Several timed-ioco variants exist: tioco of Larsen et al. [13], rtioco of Krichen and Tripakis [12], the bounded-quiescence tiocoM of Brandán Briones and Brinksma [4], and the liveness-preserving ltioco of Luthmann et al. [14], which, like us treats quiescence under composition but with a single global time-out and synchronisation hidden to internal actions.
Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO
15
Distributed systems. Closest in spirit to our work is distributed testing, where a system is observed through several interfaces. Hierons et al. adapt ioco to this setting as dioco [11], and Gaston et al. [9] give a timed distributed relation. The distinction is that distributed testing places independent (nonsynchronising) testers at the ports, so the global order of events cannot be reconstructed. In contrast, our channels are observed by a single tester, so order and per-channel quiescence remain fully recoverable. Compositionality. Compositionality of ioco has been well-studied, but most of it is untimed. The seminal work of Van der Bijl et al. [24] establishes that ioco is compositional under certain restrictions; Daca et al. [8] study compositional specifications, and van Cuyck et al. [21,22] characterise compositionality via mutual acceptance. Other compositions than parallel composition have been studied as well, e.g. merge and quotient by Beneš et al. [2], and sequential composition by Zameni et al. [25].
9
Conclusion
We presented the multi-channel lifting χM from untimed specifications to timed automata with one clock and one quiescence time-out per output channel as an extension to our previous work [6]. The lifting connects untimed multi-channel m-ioco [10] with the timed multi-channel relation m-tiocoM [5] (Theorem 1). We show that it commutes with test generation and preserves verdicts (Theorems 2 and 3). Our main contribution shows that it also commutes with sharedenvironment parallel composition (Theorem 4), which means that conformance of independently specified components carries over to the composed timed system (Corollary 2). For the modeller, it means each component may be specified in the untimed world with its own per-channel bounds and composed without the need of building the multi-channel timed model by hand. An immediate extension is to also admit internal τ -actions and enable operations such as action hiding. Internal steps let time elapse unobserved, so suspension traces and quiescence must be carefully reconstructed, as in an extension of our previous work [7]. A related direction is admitting output-to-input synchronisation in parallel composition as in [15]. This either requires input-enabledness on the synchronising actions or fragmentation of inputs into channels to keep quiescence componentwise. Acknowledgements. This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie SkłodowskaCurie grant agreement No 101008233 (MISSION). This research was supported by NWO project OCENW.M.23.155 Evidence-Driven Black-Box Checking (EVI).
16
Laura Brandán Briones
, Petra van den Bos
, and Marcus Gerhold
References 1. R. Alur. Timed automata. In N. Halbwachs and D. A. Peled, editors, Computer Aided Verification, 11th International Conference, CAV ’99, Trento, Italy, July 610, 1999, Proceedings, Lecture Notes in Computer Science, pages 8–22. Springer, 1999. 2. N. Benes, P. Daca, T. A. Henzinger, J. Kretínský, and D. Nickovic. Complete composition operators for ioco-testing theory. In P. Kruchten, S. Becker, and J. Schneider, editors, Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering, CBSE 2015, Montreal, QC, Canada, May 4-8, 2015, pages 101–110. ACM, 2015. 3. E. Brinksma, L. Heerink, and J. Tretmans. Factorized test generation for multiinput/output transition systems. In A. Petrenko and N. Yevtushenko, editors, Testing of Communicating Systems, IFIP TC6 11th International Workshop on Testing Communicating Systems (IWTCS), August 31 - September 2, 1998, Tomsk, Russia, IFIP Conference Proceedings, pages 67–82. Kluwer, 1998. 4. L. B. Briones and E. Brinksma. A test generation framework for quiescent real-time systems. In Formal Approaches to Software Testing, 4th International Workshop, FATES 2004, Linz, Austria, Revised Selected Papers, volume 3395 of LNCS, pages 64–78. Springer, 2004. 5. L. B. Briones and E. Brinksma. Testing real-time multi input-output systems. In K. Lau and R. Banach, editors, Formal Methods and Software Engineering, 7th International Conference on Formal Engineering Methods, ICFEM 2005, Manchester, UK, November 1-4, 2005, Proceedings, Lecture Notes in Computer Science, pages 264–279. Springer, 2005. 6. L. B. Briones, M. Gerhold, P. v. d. Bos, and M. Stoelinga. Time for quiescence: Modelling quiescent behaviour in testing via time-outs in timed automata. In S. Bonfanti and G. A. Papadopoulos, editors, Testing Software and Systems, pages 35–52, Cham, 2026. Springer Nature Switzerland. 7. L. B. Briones, M. Gerhold, P. van den Bos, and M. Stoelinga. Time for quiescence: Modelling quiescent behaviour in testing via time-outs in timed automata. SN Computer Science, To appear. 8. P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic. Compositional specifications for ioco testing. In Seventh IEEE International Conference on Software Testing, Verification and Validation, ICST 2014, March 31 2014-April 4, 2014, Cleveland, Ohio, USA, pages 373–382. IEEE Computer Society, 2014. 9. C. Gaston, R. M. Hierons, and P. Le Gall. An implementation relation and test framework for timed distributed systems. In H. Yenigün, C. Yilmaz, and A. Ulrich, editors, Testing Software and Systems, pages 82–97, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. 10. L. Heerink. Ins and Outs in Refusal Testing. PhD thesis, University of Twente, Enschede, Netherlands, 1998. 11. R. M. Hierons, M. G. Merayo, and M. Núñez. Implementation relations and test generation for systems with distributed interfaces. Distributed Comput., 25(1):35– 62, 2012. 12. M. Krichen and S. Tripakis. Black-box conformance testing for real-time systems. In S. Graf and L. Mounier, editors, Model Checking Software, pages 109–126, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. 13. K. G. Larsen, M. Mikučionis, and B. Nielsen. Online testing of real-time systems using UPPAAL. In J. Grabowski and B. Nielsen, editors, Formal Approaches to
Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO
17
Software Testing, 4th International Workshop, FATES, volume 3395 of Lecture Notes in Computer Science, pages 79–94. Springer, 2004. 14. L. Luthmann, H. Göttmann, and M. Lochau. Compositional liveness-preserving conformance testing of timed i/o automata. In Formal Aspects of Component Software: 16th Int. Conf., FACS 2019, Amsterdam, The Netherlands, October 23–25, 2019, Proceedings, page 147–169, Berlin, Heidelberg, 2019. Springer-Verlag. 15. N. A. Lynch and M. R. Tuttle. An introduction to input/output automata. Formal Aspects of Computing, 1988. 16. G. Stokkink, M. Timmer, and M. Stoelinga. Talking quiescence: a rigorous theory that supports parallel composition, action hiding and determinisation. In A. K. Petrenko and H. Schlingloff, editors, Proceedings 7th Workshop on Model-Based Testing, MBT 2012, Tallinn, Estonia, 25 March 2012, EPTCS, pages 73–87, 2012. 17. W. G. J. Stokkink, M. Timmer, and M. Stoelinga. Divergent quiescent transition systems. In M. Veanes and L. Viganò, editors, Tests and Proofs - 7th International Conference, TAP@STAF 2013, Budapest, Hungary, June 16-20, 2013. Proceedings, Lecture Notes in Computer Science, pages 214–231. Springer, 2013. 18. M. Timmer, E. Brinksma, and M. Stoelinga. Model-based testing. In M. Broy, C. Leuxner, and T. Hoare, editors, Software and Systems Safety - Specification and Verification, NATO Science for Peace and Security Series - D: Information and Communication Security, pages 1–32. IOS Press, 2011. 19. J. Tretmans. Model based testing with labelled transition systems. In R. M. Hierons, J. P. Bowen, and M. Harman, editors, Formal Methods and Testing, An Outcome of the FORTEST Network, Revised Selected Papers, Lecture Notes in Computer Science, pages 1–38. Springer, 2008. 20. J. Tretmans and R. Janssen. Goodbye ioco. In N. Jansen, M. Stoelinga, and P. van den Bos, editors, A Journey from Process Algebra via Timed Automata to Model Learning - Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, pages 491–511. Springer, 2022. 21. G. van Cuyck, L. van Arragon, and J. Tretmans. Compositionality in ModelBased Testing. In S. Bonfanti, A. Gargantini, and P. Salvaneschi, editors, Testing Software and Systems, pages 202–218, Cham, 2023. Springer Nature Switzerland. 22. G. van Cuyck, L. van Arragon, and J. Tretmans. Testing Compositionality. In D. Marmsoler and M. Sun, editors, Formal Aspects of Component Software, pages 39–56, Cham, 2024. Springer Nature Switzerland. 23. P. van den Bos and M. Stoelinga. Tester versus bug: A generic framework for modelbased testing via games. In A. Orlandini and M. Zimmermann, editors, Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018, Saarbrücken, Germany, 26-28th September 2018, EPTCS, pages 118–132, 2018. 24. M. van der Bijl, A. Rensink, and J. Tretmans. Compositional testing with ioco. In A. Petrenko and A. Ulrich, editors, Formal Approaches to Software Testing, Third International Workshop on Formal Approaches to Testing of Software, FATES 2003, Montreal, Quebec, Canada, October 6th, 2003, Lecture Notes in Computer Science, pages 86–100. Springer, 2003. 25. T. Zameni, P. van den Bos, J. Foederer, and A. Rensink. Sequential composition of BDD transition systems for model-based testing. In C. Ferreira and C. A. Mezzina, editors, Formal Techniques for Distributed Objects, Components, and Systems - 45th IFIP WG 6.1 International Conference, FORTE 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Lille, France, June 16-20, 2025, Proceedings, Lecture Notes in Computer Science, pages 36–54. Springer, 2025.
18
A
Laura Brandán Briones
, Petra van den Bos
, and Marcus Gerhold
Appendix: Formal Proofs
Below we provide detailed proofs to the theorems, corollaries and lemmas in the paper. The enumeration refers to the original one used in the paper. Trace prefix. Throughout, we use ⊑ to denote the trace prefix relation, i.e. given σ, σ ′ ∈ Act ∗ with σ = a1 , . . . , ak for σ ′ = a1 , . . . , an for some k ≤ n we use the notation σ ⊑ σ ′ to denote that σ ′ is a subtrace of σ. Uniformity of the lifting. The guard, reset and invariant that χM adds on a transition depend only on the channel of its action and on M (Definition 12), never on the system being lifted; and the δk self-loop exists exactly at k-quiescent states, which is what makes δk a suspension action at that state in the first place. Consequently, for a suspension trace σ that is a trace of two LTSs A and A′ , the timed realizations coincide: {ρ ∈ SttracesM (χM (A)) | ρ↓ = σ} = {ρ ∈ SttracesM (χM (A′ )) | ρ↓ = σ}. In particular, since the valuation reached after a timed trace ρ is determined by ρ (there are no τ -steps), whether a step (d, a) is admissible after ρ depends only on ρ, M, and whether a is enabled at the reached state in the untimed system. We refer to this as uniformity of the lifting. Lemma 1 (Multi-channel canonic traces). Let A = ⟨S, Act, →, s0 ⟩ be an LTS with an n-channel output partition and M = [M1 , . . . , Mn ] ∈ Rn>0 , then: If ρ ∈ SttracesM (χM (A)), then there is σ ∈ Straces(A) such that ρ↓ = σ. Proof. The proof is by construction. Let ρ ∈ SttracesM (χM (A)). By Definition 10 any suspension timed trace can be written as (d1 ,a1 )
(d2 ,a2 )
(dm ,am )
ℓ0 −−−−→ ℓ1 −−−−→ . . . −−−−−→ ℓm , and, since ρ ∈ SttracesM (χM (A)), every step is a genuine timed transition of χM (A), i.e. its guards hold and its location invariants are respected throughout the elapsed delay. By Definition 12 every transition in →χM (A) extends a discrete transition of A with a guard, an invariant, and a reset, or is an added δk self-loop at a k-quiescent location; explicitly, each has one of the forms: V – (ℓ, i?, k ck < Mk , C, ℓ′ ) for inputs (s, i?, s′ ) ∈→A with i? ∈ Act I ; – (ℓ, o!, ck < Mk , {ck }, ℓ′ ) for outputs (s, o!, s′ ) ∈→A with o! ∈ Act kO ; – (ℓ, δk , ck = Mk , {ck }, ℓ) for k-quiescent locations. The projection ρ↓ deletes the delays dj ∈ R≥0 , which are the only information not present in A, leaving the sequence σ = a1 a2 . . . am . We argue that σ ∈ Straces(A) by following the suspended timed trace step-bystep. Since L = S, each ℓj identifies a state sj (w.l.o.g. otherwise rename the ℓ but keep the location-to-location transitions in place), and for each step we read off the matching transition of A, that is:
Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO
19
– if aj ∈ Act I ∪ Act O , the corresponding lifted transition extends a discrete aj transition sj−1 −→ sj of A, which is therefore present in σ; – if aj = δk , the step took the lifted self-loop, which by Definition 12 exists only at a k-quiescent location. By Definition 10 the step is admissible only if ℓj−1 is k-quiescent, so sj−1 is k-quiescent (cf. Definition 9) and contributes δk to its suspended traces. Hence every action of σ is admissible in A in the order it appears, so σ ∈ Straces(A) with ρ↓ = σ. Moreover, then by Definition 13 σ ∈ TStraces(A). ⊓ ⊔ Corollary 1 (Input-enabledness under χM ). χM maps IOTSs to IOTAs. Proof. By Definition 12, the lifting adds on every input transition the guard Vn c k=1 k < Mk . This guard is satisfied at exactly those valuations v with vk < Mk for all k, which is precisely the condition under which an IOTA is required to be input-enabled (Definition 8). Since an IOTS enables every input at every state, and the lifting preserves states and adds these input transitions, every location of χM (AI ) enables every input at every such valuation. Hence, if AI is an IOTS then χM (AI ) is an IOTA. ⊔ ⊓ Theorem 1 (Preservation). Let AI be an IOTS and AS an LTS over the same n-channel output partition. For every M = [M1 , . . . , Mn ] ∈ Rn>0 : AI m-iocoM AS if and only if χM (AI ) m-tiocoM χM (AS ). Proof. Let M ∈ Rn>0 and write AI = χM (AI ), AS = χM (AS ). Since AI is an IOTS, AI is an IOTA (Corollary 1). W.l.o.g. we identify each state with its location, since L = S under χM (Definition 12). We first record how untimed and timed observables relate. Therefore, let ρ ∈ SttracesM (AS ) and σ = ρ↓; by Lemma 1, σ ∈ TStraces(AS ). Let v be the valuation reached after ρ, which is the same in AI and AS (via uniformity of the lifting, see above). For a ∈ Act kO ∪ {δk } and either system A ∈ {AI , AS } with lifting A, Definition 10 gives that some (d, a) ∈ out M k (A after ρ) iff ρ · (d, a) ∈ SttracesM (A) iff σ · a ∈ TStraces(A) via ρ · (d, a). That is, T {a | ∃d (d, a) ∈ out M k (A after ρ)} ⊆ out k (A, σ),
(1)
and conversely, if σ·a ∈ TStraces(A) then by uniformity every realization of σ, in particular ρ, extends to a realization of σ·a, so some (d, a) lies in out M k (Aafterρ). Hence (1) is an equality. Finally, for a fixed a the set of admissible d after ρ depends only on v, M and the guard form of a (uniformity), and is therefore the same for AI and AS whenever a is enabled in both. ⇒ Assume AI m-iocoM AS . Let ρ ∈ SttracesM (AS ), σ = ρ↓, and (d, a) ∈ T T out M k (AI afterρ). By (1) for AI , a ∈ out k (AI , σ); by m-iocoM , a ∈ out k (AS , σ); M ′ by the converse of (1) for AS , some (d , a) ∈ out k (AS after ρ), and since the admissible delays for a coincide on both sides, (d, a) ∈ out M k (AS after ρ). Hence AI m-tiocoM AS .
20
Laura Brandán Briones
, Petra van den Bos
, and Marcus Gerhold
⇐ Assume AI m-tiocoM AS . Let σ ∈ TStraces(AS ) and a ∈ out Tk (AI , σ), i.e. σ · a ∈ TStraces(AI ) via some ρ · (d, a) ∈ SttracesM (AI ) with ρ↓ = σ. As σ ∈ Straces(AS ), uniformity gives ρ ∈ SttracesM (AS ). Now (d, a) ∈ out M k (AI after ρ), so by m-tiocoM also (d, a) ∈ out M (A afterρ), i.e. ρ·(d, a) ∈ Sttraces S M (AS ), k with σ · a ∈ TStraces(AS ) and a ∈ out Tk (AS , σ). Hence AI m-iocoM AS . For the final claim, AI m-iocoAS implies AI m-iocoM AS (Definition 14), hence AI m-tiocoM AS by the first direction. ⊓ ⊔ Theorem 2 (Test correspondence). Let TLTS (AS ) be the set of test cases for an LTS AS (Definition 15) and TTA (χM (AS )) the set of timed test cases for χM (AS ) (Definition 16). Then: χM (TLTS (AS )) = TTA (χM (AS )). Proof. Recall that on test cases χM decorates the existing transitions and adds none (Section 6), so pass and fail remain terminal (specifically, no δ are added. The proof is in two steps via set inclusion in both direction, i.e. case (1) χM (TLTS (AS )) ⊆ TTA (χM (AS )) and case (2) TTA (χM (AS )) ⊆ χM (TLTS (AS )). χM (TLTS (AS )) ⊆ TTA (χM (AS )) Let t ∈ TLTS (AS ) and put tTA = χM (t). We verify each clause of Definition 16 to show that tTA ∈ TTA (χM (AS )) is a timed test case. Structure. χM is structure preserving, so tTA has the same actions and the δk , already present in t by Definition 15, the same tree shape, and the same finite, acyclic, deterministic structure. The δk transitions in a test case lead to successor states, not self-loops (cf. Definition 15), so acyclicity is preserved. Further, pass, fail have no outgoing transitions in t; χM adds none, so they are terminal in tTA . Every transition of tTA lies on a timed trace: a transition of t lies on some σ ∈ traces(t) ending in an input, pass or fail; by input-specifiedness resp. soundness that trace (or its prefix before the final output) is in TStraces(AS ), hence realizable, and the final step is realizable by uniformity of the lifting. M Clocks and invariants. V By construction χ adds the clocks C = {c1 , . . . , cn } and the invariant k ck ≤ Mk at every non-terminal location, as required. Observation/stimulation and per-channel guards. Each non-terminal state of t enables either all of Act O ∪ {δ1 , . . . , δn } (observe) or Act O and one input (stimulate) (cf. Definition 15). Under χM these become output transitions guarded by ck < Mk or δk transitions guarded by ck = Mk , or the output V transitions plus a single input guarded k ck < Mk with reset C. These are exactly the guard/reset forms required by Definition 16. Input-specifiedness, soundness, correctness. For input-specifiedness, let ρ· (d , i?) ∈ ttraces(tTA ). Its projection ρ↓ · i? lies in traces(t), hence by inputspecifiedness of t in TStraces(AS ) ⊆ Straces(AS ). By uniformity, the realization ρ · (d , i?) of this trace in tTA is also a realization in χM (AS ), i.e. ρ · (d , i?) ∈ SttracesM (χM (AS )). Soundness transfers identically, i.e. a timed
Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO
21
trace of tTA reaching pass projects to a trace of t reaching pass, which lies in TStraces(AS ), and uniformity places the timed trace in SttracesM (χM (AS )). For correctness, let ρ · (d , o) ∈ ttraces(tTA ) reach fail. Its projection reaches fail in t, so by correctness of t it is not in TStraces(AS ); by Definition 13 it therefore has no realization in χM (AS ), and therefore in particular ρ·(d , o) ∈ / SttracesM (χM (AS )). All properties together yield χM (t) = tTA ∈ TTA (χM (AS )). χM (TLTS (AS )) ⊇ TTA (χM (AS )) Let tTA ∈ TTA (χM (AS )) and let t = tTA ↓, i.e. its projection by erasing clocks, invariants, guards, and resets, but keeping locations (resp. states), the initial location, and the labelled transition relation. We now show χM (t) = tTA and t ∈ TLTS (AS ). By Definition 16, V every transition of tTA has one of the three canonic forms (1) input guarded by k ck < Mk reset C; (2) channel-k output guarded ck < Mk reset {cV k }, or (3) δk guarded ck = Mk reset {ck }, and every non-terminal location carries k ck ≤ Mk . These are precisely the decorations χM adds (Definition 12). Since the projection t keeps exactly the discrete transitions and δk occurs in tTA as an ordinary transition (rather than being added by χM ), re-applying χM restores every guard, reset and invariant. Hence χM (t) = tTA . The projection tTA ↓ is tree-shaped, finite, acyclic, and deterministic because tTA is, these being properties of the discrete structure. The terminal states and the observe/stimulate options are read off directly: an observe location (enabling all outputs and all δk ) projects to an observe state; a stimulate location (enabling all outputs and one input) projects to a stimulate state. For the remaining conditions, note that since every transition of tTA lies on a timed trace (Definition 16), every σ ∈ traces(t) is the projection of some ρ ∈ ttraces(tTA ). Input-specifiedness: if σ · i? ∈ traces(t) then some ρ · (d , i?) ∈ ttraces(tTA ) projects to it, which by input-specifiedness of tTA lies in SttracesM (χM (AS )), so σ · i? ∈ TStraces(AS ) by Definition 13. Soundness is identical. Correctness: if σ · o ∈ traces(t) reaches fail, then every realization ρ · (d , o) ∈ ttraces(tTA ) reaches fail and by correctness of tTA is not in SttracesM (χM (AS )); as this holds for every realization, σ · o ∈ / TStraces(AS ). Hence t ∈ TLTS (AS ), and tTA = χM (t) ∈ χM (TLTS (AS )). Both inclusions hold, so χM (TLTS (AS )) = TTA (χM (AS )).
⊔ ⊓
Theorem 3 (Verdict preservation). For every IOTS AI and LTS AS and every M = (M1 , . . . , Mn ) ∈ Rn>0 : 1. If AI passes TLTS (AS ), then χM (AI ) passes TTA (χM (AS )). 2. If AI fails TLTS (AS ), then χM (AI ) fails TTA (χM (AS )). Proof. Let M ∈ Rn>0 and write AI = χM (AI ) and AS = χM (AS ). Recall from LTS-test verdicts (text below Definition 15) that AI fails a test t iff some σ ∈ TStraces(AI ) ∩ traces(t) reaches fail, and passes otherwise; likewise AI fails a timed test tTA iff some ρ ∈ SttracesM (AI ) ∩ ttraces(tTA ) reaches fail. Since a
22
Laura Brandán Briones
, Petra van den Bos
, and Marcus Gerhold
test case carries δ1 , . . . , δn in its alphabet (Definition 15), its suspension traces coincide with its traces. By Theorem 2, every timed test case for χM (AS ) is χM (t) for a t ∈ TLTS (AS ), and vice versa. We use this bijection to prove the preservation of verdicts, i.e. for a test t and its lifting tTA = χM (t), a testable trace reaches fail in t while being a trace of AI iff its timed trace reaches fail in tTA while being a trace of AI : σ
∃ σ ∈ TStraces(AI ) ∩ traces(t) : t − → fail ρ
⇐⇒ ∃ ρ ∈ SttracesM (AI ) ∩ ttraces(tTA ) : tTA = ⇒ fail.
(2)
σ
→ fail. By Definition 13 there ⇒ Given is σ ∈ TStraces(AI ) ∩ traces(t) with t − is ρ ∈ SttracesM (AI ) with ρ↓ = σ. Since σ ∈ traces(t) and tTA = χM (t) adds the same canonic guards as AI , uniformity gives ρ ∈ ttraces(tTA ). Since fail is reached in t along σ, it is reached in tTA = χM (t) along ρ, because χM maps the discrete transition into fail to the corresponding timed transition into fail. ⇐ This case is symmetrical and we project ρ by ↓. The resulting projection σ is in TStraces(AI ) (by Lemma 1) and a trace of t (since tTA = χM (t) retains exactly the discrete transitions), and reaches fail in t. (1) Preservation of passing. The proof is by contraposition. Suppose AI = χM (AI ) fails TTA (χM (AS )). Then some tTA ∈ TTA (χM (AS )) has a trace of AI reaching fail, i.e. the right side of (2) holds. By Theorem 2, tTA = χM (t) for some t ∈ TLTS (AS ), so (2) gives a AI -trace reaching fail in t. Hence AI fails t, and therefore does not pass TLTS (AS ). (2) Preservation of failing. Suppose AI fails TLTS (AS ), i.e. some t ∈ TLTS (AS ) has a trace of AI reaching fail in t. Then tTA = χM (t) ∈ TTA (χM (AS )) by Theorem 2, and the left side of (2) holds, so the right side gives an AI -trace reaching fail in tTA . Hence AI fails tTA , and therefore fails TTA (χM (AS )). ⊓ ⊔ Theorem 4 (Compositionality). Let A1 , A2 be LTSs with disjoint output 1 2 alphabets and shared inputs, and let M1 ∈ Rn>0 , M2 ∈ Rn>0 . Then χM1 ⌢M2 (A1 ∥ A2 ) = χM1 (A1 ) ∥ χM2 (A2 ). Proof. Let A1 ∥ A2 = ⟨S1 × S2 , Act, →∥ , (s0,1 , s0,2 )⟩ be the composed system as per Definition 17 and recall that its output partition is the disjoint union of the two component partitions, with A1 channels indexed 1, . . . , n1 and A2 ’s channels indexed n1 + 1, . . . , n1 + n2 . Under this indexing the bound vector of the composition is exactly M1 ⌢ M2 , and χM [M1 ⌢ M2 ] introduces clocks c1 , . . . , cn1 +n2 . We show the two sides of the equation have identical locations, clocks, transitions and invariants, which ultimately proves their equivalence. Locations and clocks. Both sides have location set S1 × S2 and initial location (s0,1 , s0,2 ): the left by L = S of χM (Definition 12) applied to A1 ∥ A2 , and the right by the product of Definition 18. Both have clock
Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO
23
set {c1 , . . . , cn1 +n2 }: the left because the composed partition has n1 + n2 channels, the right because Definition 18 takes the union of the component clock sets. The clock indexing coincides by the convention above. Input transitions. Recall that we stipulate that all inputs are shared between all composing systems, and let i? ∈ Act sync be such a shared input. On the I i?
i?
left, A1 ∥ A2 synchronises it (Definition 17): (ℓ1 , ℓ2 ) −→ (ℓ′1 , ℓ′2 ) iff ℓ1 −→ ℓ′1 Vn1 +n2 i? and ℓ2 −→ ℓ′2 . Lifting, χM1 ⌢M2 gives guard k=1 ck < (M1 ⌢ M2 )k and reset of all clocks. On the right, i? is lifted within each component, i.e. V n2 V n1 cn1 +k < (M2 )k , each resetting all of its ck < (M1 )k and k=1 guard k=1 own clocks. The synchronisation clause of 18 joins the guards and VnDefinition 1 +n2 ck < (M1 ⌢ M2 )k and the unifies the resets. The joined guard is k=1 unified reset is all of {c1 , . . . , cn1 +n2 }, matching the left. Output transitions. Let o! ∈ Act kO (A1 ), so k ≤ n1 . Outputs are disjoint, so o! belongs to A1 and is not shared with A2 by assumption. On the left, o! is a transition of A1 ∥ A2 via the interleaving clause of Definition 17: o!
o!
(ℓ1 , ℓ2 ) − → (ℓ′1 , ℓ2 ) iff ℓ1 − → ℓ′1 in A1 . Lifting it, χM1 ⌢M2 gives guard ck < o!
(M1 ⌢ M2 )k = (M1 )k and reset {ck }. On the right, the same ℓ1 − → ℓ′1 M1 is first lifted by χ to guard ck < (M1 )k , reset {ck }, then carried into the product by the interleaving clause of Definition 18. The two transitions coincide. Outputs of A2 are symmetric, with channel index shifted by n1 . Quiescence self-loops. Let k ≤ n1 (the case k > n1 is symmetric). We claim (ℓ1 , ℓ2 ) is k-quiescent in A1 ∥ A2 iff ℓ1 is k-quiescent in A1 . A channel-k output can be enabled at (ℓ1 , ℓ2 ) only via the interleaving clause from A1 (outputs are disjoint, so A2 has no channel-k output; shared inputs synchronise to inputs and not outputs, and by Definition 17 no output of one component is an input of the other). Hence a channel-k output is enabled at (ℓ1 , ℓ2 ) iff it is enabled at ℓ1 , so the two states agree on k-quiescence. On the left, χM1 ⌢M2 therefore adds the self-loop ⟨(ℓ1 , ℓ2 ), δk , ck = (M1 ⌢ M2 )k , {ck }, (ℓ1 , ℓ2 )⟩ iff ℓ1 is k-quiescent. On the right, χM [M1 ] adds ⟨ℓ1 , δk , ck = (M1 )k , {ck }, ℓ1 ⟩ iff ℓ1 is k-quiescent, and Definition 18 carries this self-loop into the product as a δk loop at (ℓ1 , ℓ2 ). Since it is non-shared it interleaves and leaves ℓ2 fixed. Since (M1 ⌢ M2 )k = (M1 )k , the two quiescent self-loops coincide. Invariants.VOn the left, the lifting χM1 ⌢M2 assigns to every location the inn1 +n2 variant k=1 ck ≤ (M1 ⌢ M2 )k where (M1 ⌢ M2 )k is the k-th position of the vector. On the right,VDefinition 18 assigns Vn(ℓ2 1 , ℓ2 ) the conjunction of n1 the component invariants, k=1 ck ≤ (M1 )k ∧ k=1 cn1 +k ≤ (M2 )k . Since (M1 ⌢ M2 )k = (M1 )k for k ≤ n1 and (M1 ⌢ M2 )n1 +k = (M2 )k for k ≤ n2 , the two invariants are identical. The two timed automata are identical because all four ingredients coincide. ⊔ ⊓ Lemma 2 (Compositionality of testable multi-ioco). Let A1I , A1S and let A2I , A2S be the implementation–specification pairs of LTSs, with A1I , A2I IOTSs. Assume they have disjoint outputs (Act O,1 ∩ Act O,2 = ∅) and shared inputs,
24
Laura Brandán Briones
, Petra van den Bos
, and Marcus Gerhold
2 1 . If A1I m-iocoM1 A1S and and M2 ∈ Rn>0 and have bound vectors M1 ∈ Rn>0 2 2 1 2 AI m-iocoM2 AS , then AI ∥ AI m-iocoM1 ⌢M2 A1S ∥ A2S .
Proof. Let I = A1I ∥ A2I and S = A1S ∥ A2S . By Definition 14 we must show, for every σ ∈ TStraces[M1 ⌢ M2 ](S) and every channel k ∈ {1, . . . , n1 + n2 }, that out Tk [M1 ⌢ M2 ](I, σ) ⊆ out Tk [M1 ⌢ M2 ](S, σ). Projection. For a suspension trace σ of S and i ∈ {1, 2}, let σ|i be its projection onto Act δAi . By Definition 17, shared inputs advance both components and every other action advances exactly one, so σ|i ∈ Straces(AiS ), and S after σ consists of pairs (s1 , s2 ) with si ∈ AiS after σ|i ; likewise for I. Moreover σ|i is testable for Mi : a witness ρ ∈ SttracesM1 ⌢M2 (χM1 ⌢M2 (S)) for σ is, by Theorem 4, a timed trace of χM1 (A1S ) ∥ χM2 (A2S ), and its projection ρ|i onto component i (dropping the other component’s actions and accumulating their delays) is a timed trace of χMi (AiS ) with ρ|i ↓ = σ|i . Hence σ|i ∈ TStraces[Mi ](AiS ), and the same argument shows that σ · a ∈ TStraces[M1 ⌢ M2 ](I) implies σ|i ·a ∈ TStraces[Mi ](AiI ) for any a owned by component i. Note that the bound of a channel is unchanged by concatenation, i.e. if channel k of the composition is owned by component i, then (M1 ⌢ M2 )k = (Mi )k′ for the corresponding index k ′ in that component. We note that the projection is well defined: component i’s clocks are reset only by its own outputs, by δk with k owned by i, and by inputs, which are shared and hence kept. Dropped steps therefore only let time pass, so component i’s valuation evolves identically in ρ and ρ|i . Moreover the composite guards and invariant imply the component ones (they are conjunctions over a superset of channels), so every kept step remains admissible at its accumulated delay, and the component invariant holds throughout it. Factoring. Let channel k be owned by component i; ownership is unique since output partitions are disjoint. As in the proof of Theorem 4, a channel-k output is enabled at (s1 , s2 ) iff it is enabled at si , and (s1 , s2 ) is k-quiescent iff si is. Conclusion. Fix σ ∈ TStraces[M1 ⌢ M2 ](S), a channel k owned by i, and a ∈ out Tk [M1 ⌢ M2 ](I, σ), i.e. σ·a ∈ TStraces[M1 ⌢ M2 ](I) via some ρ·(d, a) ∈ SttracesM [M1 ⌢ M2 ](χM1 ⌢M2 (I)). By projection, σ|i ∈ TStraces[Mi ](AiS ) and σ|i · a ∈ TStraces[Mi ](AiI ), so a ∈ out Tk [Mi ](AiI , σ|i ). By the hypothesis AiI m-iocoMi AiS , we get a ∈ out Tk [Mi ](AiS , σ|i ), in particular σ|i · a ∈ Straces(AiS ), so a is enabled (resp. AiS is k-quiescent) at AiS after σ|i , and by factoring the same holds at S after σ. It remains to realize σ · a in χM1 ⌢M2 (S). By uniformity, ρ ∈ SttracesM [M1 ⌢ M2 ](χM1 ⌢M2 (S)) (as σ ∈ Straces(S)), and the step (d, a) is admissible after ρ in χM1 ⌢M2 (S) iff a is enabled at S after σ and the guard and invariant, which are the same canonic constraints as in χM1 ⌢M2 (I), hold for d; both conditions are met. Hence ρ·(d, a) ∈ SttracesM [M1 ⌢ M2 ](χM1 ⌢M2 (S)), so σ · a ∈ TStraces[M1 ⌢ M2 ](S) and a ∈ out Tk [M1 ⌢ M2 ](S, σ). As σ, k and a were arbitrary, I m-iocoM1 ⌢M2 S. ⊓ ⊔ Corollary 2 (Composition of timed conformance). Let A1I , A1S and A2I , A2S be implementation–specification pairs of LTSs, with A1I , A2I IOTSs. Assume the pairs have disjoint outputs (Act O,1 ∩ Act O,2 = ∅) and shared inputs, and have
Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO
25
2 1 . If A1I m-iocoM1 A1S and A2I m-iocoM2 , M2 ∈ Rn>0 bound vectors M1 ∈ Rn>0 2 M1 ⌢M2 1 2 AS , then χ (AI ∥ AI ) m-tiocoM1 ⌢M2 χM1 ⌢M2 (A1S ∥ A2S ).
Proof. By Lemma 2, A1I ∥ A2I m-iocoM1 ⌢M2 A1S ∥ A2S . Further, A1I ∥ A2I is an IOTS because parallel composition preserves input-enabledness (all inputs are shared and enabled in every state of both components, so every synchronised input is enabled in every product state). Then, by Corollary 1 its lifting is an IOTA and m-tiocoM1 ⌢M2 is well-typed. Applying Theorem 1 to the composed systems with bound vector M1 ⌢ M2 gives χM1 ⌢M2 (A1I ∥ A2I ) m-tiocoM1 ⌢M2 χM1 ⌢M2 (A1S ∥ A2S ). ⊔ ⊓