PaperlayerView exact revision on arXiv

Source-linked AI summary

Quiescence in Concert: Composing Multi-Channel Time-Outs for IOCO

Laura Brandán Briones, Petra van den Bos, Marcus Gerhold

arXiv:2609.17640v1cs.SEcs.FL

TL;DR

A single global time-out can misrepresent quiescence when channels have different bounds. The paper introduces a multi-channel lifting from untimed specifications to timed automata, then shows that conformance, testing, verdicts, and parallel composition are preserved on tester-observable traces.

  • Problem

    A single global time-out can prematurely declare a slower channel quiescent, delay faster-channel verdicts, and obscure which channel is silent.

    Source: §1 · p. 2

  • Method

    The multi-channel lifting assigns each output channel its own clock and time-out, connecting untimed m-ioco to timed m-tiocoM.

    Source: §1 · p. 2

  • Results

    The lifting commutes with test generation and shared-environment parallel composition, preserves test verdicts, and bridges the untimed and timed conformance relations.

    Source: §9 · p. 15

  • Takeaways & Limitations

    Components can be specified untimed with their own per-channel bounds and composed for timed testing without building the timed models by hand.

    Source: §7 · p. 12, §9 · p. 15

    The preservation correspondence is limited to testable suspension traces, since some trace orderings cannot be observed by a time-out-based tester.

    Source: §5 · p. 9

Abstract

from arXiv · show

In Model-Based Testing (MBT), test suites are generated automatically from a formal specification. The theory of testing real-time 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.

1 Introduction

The introduction motivates per-channel time-outs because one global deadline can misclassify or delay quiescence and erase which channel is silent. It presents a multi-channel lifting that connects untimed and timed conformance while preserving testing operations and parallel composition.

1 Introduction

  • A single global time-out can declare a slow channel quiescent too early, delay faster-channel verdicts, and collapse distinct channel-quiescence labels.Choosing the minimum deadline accepts implementations the specification rejects; choosing the maximum delays faster-channel observations.Source: §1 · p. 2
  • The introduction positions the work as a bridge from untimed component specifications to multi-channel timed testing, building on prior single-time-out lifting.The prior lifting preserves ioco, commutes with test generation, and preserves test verdicts.Source: §1 · pp. 1–2
  • The multi-channel lifting gives each output channel its own clock and quiescence time-out, bridging untimed m-ioco and timed m-tiocoM.The lifting also commutes with test generation, preserves verdicts, and commutes with shared-environment parallel composition.Source: §1 · p. 2
  • Per-channel bounds can order suspension-trace quiescence in ways a time-out-based tester cannot produce, so the correspondence is restricted to testable traces.The paper defines testable traces to address this mismatch.Source: §1 · p. 2
  • The paper overview assigns the lifting and conformance bridge to Section 5, testing results to Section 6, and compositionality to Section 7.Sections 2–4 establish LTS, multi-channel ioco, timed automata, and m-tiocoM.Source: §1 · pp. 2–3

2 Labelled Transition Systems

This section sets up labelled transition systems and makes the input-enabled assumption explicit for implementation models. It excludes internal τ-actions for simplicity.

2 Labelled Transition Systems

  • The presentation excludes internal τ-actions for simplicity, while noting their inclusion is not expected to cause issues.Inputs and outputs are distinguished by naming conventions, not by adding suffixes to the labels themselves.Source: §2 · p. 3
  • An LTS has a finite state set, an action alphabet, a transition relation, and a unique initial state.Transitions carry action labels; traces are sequences of actions that can be followed from a state.Source: §2 · p. 3
  • Implementations are assumed input-enabled: a tester can provide any input at any time.The paper calls input-enabled LTSs input-output transition systems (IOTSs).Source: §2 · p. 3

3 Multi-channel ioco

This section extends ioco to systems whose outputs are partitioned into channels, with a distinct quiescence observation for each channel. The resulting relation checks implementation outputs channel by channel after specification suspension traces.

3 Multi-channel ioco

  • Output channels partition the output alphabet into disjoint sets, while inputs remain shared across components.The paper motivates this choice by treating quiescence as an output observation: testers control inputs but observe whether outputs occur.Source: §3 · p. 3
  • A state is k-quiescent when it has no outgoing output on channel k; each channel receives its own δk observation in suspension traces.Classical quiescence holds when the state is quiescent on every channel.Source: §3 · p. 4
  • Multi-channel ioco checks, after every specification suspension trace, that implementation outputs on each channel are included in the specification’s outputs on that channel.With one output channel, the relation reduces to classical ioco.Source: §3 · p. 4
  • The ATM display example has inputs card? and pin? and channel-1 outputs msg! and err!; quiescence loops mark states without enabled outputs.The plain LTS is not input-enabled, and the example is later composed with a cash dispenser to form a two-channel system.Source: §3 · pp. 4–5

4 Timed Automata and Multi-Channel m-tiocoM

This section recalls timed automata and defines timed multi-channel conformance using a bound for each channel. Input-enabledness is required before the relevant quiescence bounds are reached.

4 Timed Automata and Multi-Channel m-tiocoM

  • A timed automaton uses locations with clock invariants and guarded transitions that may reset clocks; the paper excludes Zeno behaviour.A transition is enabled when its guard holds, and its clock resets occur when the transition is taken.Source: §4 · p. 5
  • Timed traces pair non-negative delays with visible actions, and the section defines clock constraints using comparisons between clocks and bounds.A clock valuation assigns each clock its current non-negative value.Source: §4 · p. 5
  • The vector M supplies one positive quiescence bound per channel, and input-enabledness is required while every channel remains below its bound.Once a channel reaches its bound, it must conclude quiescence; the input-enabledness requirement therefore applies only before that point.Source: §4 · pp. 5–6
  • Timed k-quiescence concerns whether a channel’s output transitions are enabled, independently of clock valuation.The section states this condition via a delay rather than a valuation.Source: §4 · p. 6
  • The timed relation m-tiocoM compares implementation outputs against specification outputs after timed suspension traces, separately for every channel.The section presents the relation as matching the multi-channel timed relation of in spirit, with a single shared input channel.Source: §4 · pp. 6–7

5 The Canonic Multi-Channel Lifting χM

The multi-channel lifting gives each output channel its own clock and quiescence bound. It preserves the conformance correspondence with timed multi-channel ioco when traces are restricted to those a time-out tester can observe.

5 The Canonic Multi-Channel Lifting χM

  • χM assigns one clock and one quiescence time-out to each output channel, with a separate bound Mk.The lifted automaton uses location invariants ck ≤ Mk, channel-k output guards ck < Mk, and δk guards ck = Mk.Source: §5 · p. 7
  • Inputs reset all channel clocks, whereas an output on channel k resets only ck because it gives no evidence of activity on other channels.At each channel’s bound, the invariant prevents further time until that channel’s δk is observed.Source: §5 · p. 7, Table 1 · p. 8
  • The lifting maps channel-k outputs to timed observations before Mk and k-quiescence to an observation at Mk, matching untimed and timed observations per channel.Erasing delays from a lifted trace yields a trace of the original LTS.Source: §5 · p. 8
  • The reverse trace correspondence is restricted to testable traces, excluding sequences such as δ2o1 when M1 < M2 because a faster channel’s timeout cannot be skipped.Restricting m-ioco to testable traces yields a relation that matches m-tiocoM.Source: §5 · p. 9

6 Test Cases and Commutation

The paper defines multi-channel tests for untimed and timed models, with quiescence observed separately on each channel. Lifting commutes with test generation and preserves pass/fail verdicts for lifted tests and implementations.

6 Test Cases and Commutation

  • Multi-channel tests distinguish quiescence observations δ1, …, δn, while testers may stop, observe outputs or quiescence, or provide an input.LTS tests are finite, deterministic, and acyclic; timed tests use one clock per output channel.Source: §6 · pp. 9–10
  • Per-channel observe states can yield smaller, targeted tests, but faults on an ignored channel must be detected elsewhere in the test suite.Tests depend on M through the testable traces that a time-out-based tester can observe.Source: §6 · p. 10
  • Lifting commutes with test generation: lifting the untimed test cases gives the timed test cases for the lifted specification.The lifting decorates existing test transitions and leaves pass and fail terminal.Source: §6 · p. 11
  • An implementation passes the untimed test cases if and only if its lifting passes the timed test cases, and failure is preserved as well.The theorem states both pass and fail preservation for every IOTS and LTS under the channel bounds.Source: §6 · p. 11

7 Compositionality

The multi-channel lifting commutes with shared-environment parallel composition, so components can retain their own quiescence bounds when composed. The result applies to components with disjoint outputs and shared inputs.

7 Compositionality

  • Lifting the composed specification yields the composition of the lifted components, up to clock renaming.This compositionality result lets components keep their own per-channel bounds without building a global timed model by hand.Source: §7 · pp. 12, 14
  • The composition assumes shared inputs and disjoint output alphabets, with each component’s output partition and bound retained.The composed timed automata use disjoint clock sets and component-wise joined invariants.Source: §7 · p. 12
  • In the ATM example, the UI and dispenser have quiescence bounds of 1 and 5 time units, respectively.The components synchronize on card? and pin?; states may be quiescent on both channels or have outputs enabled on both.Source: §7 · p. 13, Figure 3 · p. 13
  • A single global timeout makes fast-channel quiescence wait for the slowest channel, whereas per-channel clocks let each channel conclude at its own bound.The paper states this avoids the time overhead of waiting out the slowest channel everywhere.Source: §7 · pp. 13–14

8 Related Work

Related work spans quiescence, timed and multi-channel conformance, and compositionality. This paper extends prior lifting work to multi-channel systems and differs from distributed testing in how observations are recovered.

8 Related Work

  • The paper extends the authors’ prior work on timed lifting to the multi-channel setting.The surrounding work also builds on ioco and quiescent transition systems [16].Source: §8 · p. 14
  • Heerink introduced untimed multi-channel refusal testing, while Brandán Briones and Brinksma gave a timed multi-input/output relation.The cited work differs in its treatment of input channels and timed labelled transition systems.Source: §8 · p. 14
  • Timed testing includes rtioco, bounded-quiescence tiocoM, and liveness-preserving ltioco, which treats quiescence under composition with a single global time-out and synchronisation hidden to internal actions.Source: §8 · p. 14
  • Unlike distributed testing with independent testers, this work uses one tester, so global event order and per-channel quiescence remain recoverable.The cited distributed-testing approaches include dioco and a timed distributed relation.Source: §8 · p. 15
  • Prior compositionality work is mostly untimed, including restricted ioco composition and studies of compositional specifications and mutual acceptance [21].Other studied compositions include merge and quotient and sequential composition.Source: §8 · p. 15

9 Conclusion

The paper presents a multi-channel lifting connecting untimed and timed conformance, and shows that it commutes with shared-environment composition. It identifies internal actions and output-to-input synchronization as extension directions.

9 Conclusion

  • The multi-channel lifting assigns one clock and quiescence timeout per output channel, connecting m-ioco with m-tiocoM.This extends the authors’ earlier lifting.Source: §9 · p. 15
  • The lifting commutes with test generation and preserves test verdicts.The paper attributes these results to Theorems 2 and 3.Source: §9 · p. 15
  • It commutes with shared-environment parallel composition, so conformance of independently specified components carries over to the composed timed system.Components can be specified untimed with per-channel bounds without manually constructing the multi-channel timed model.Source: §9 · p. 15
  • Internal τ-actions, action hiding, and output-to-input synchronization remain extension directions; the latter requires input-enabledness or channelized inputs.Internal steps would require careful reconstruction of suspension traces and quiescence.Source: §9 · p. 15

A Appendix: Formal Proofs

The appendix proves preservation results for multi-channel lifting across traces, conformance, testing, verdicts, and composition, including compositional conformance. It also establishes conditions for applying timed conformance to composed systems, using uniform timed realizations and projection between timed traces and untimed suspension traces.

A Appendix: Formal Proofs

  • Every timed suspension trace of the lifted LTS projects, after erasing delays, to an untimed suspension trace of the original LTS.The construction reads each projected action from an original transition or a lifted quiescence loop at a quiescent state.Source: A Appendix: Formal Proofs · pp. 18–19
  • Lifting an IOTS yields an IOTA because lifted input transitions are enabled whenever all channel clocks are below their bounds.This guard is the condition for input-enabledness in an IOTA, and the lifting preserves states while adding input transitions.Source: A Appendix: Formal Proofs · p. 19
  • Untimed and timed conformance are preserved by the lifting, with the proof relating outputs and admissible delays along testable traces.The lifting’s uniformity makes timed realizations and admissible delays depend on the trace, bounds, and enabled actions rather than on which system is lifted.Source: A Appendix: Formal Proofs · pp. 19–20
  • Theorem 2 establishes a correspondence between untimed test cases and timed test cases for the lifted specification.The proof gives inclusions in both directions, using the fact that lifting decorates existing test transitions without adding transitions.Source: A Appendix: Formal Proofs · p. 20
  • Passing and failing test verdicts are preserved when implementations, specifications, and tests are lifted.The proof uses the correspondence between test cases and matches testable traces reaching fail in the untimed and timed tests.Source: A Appendix: Formal Proofs · pp. 21–22
  • Lifting commutes with parallel composition for components with disjoint output alphabets and shared inputs.The proof shows that the two constructions have identical locations, clocks, transitions, and invariants.Source: A Appendix: Formal Proofs · pp. 22–23
  • The appendix proves compositionality of testable multi-ioco for implementation–specification pairs with disjoint outputs and shared inputs.The proof projects composite suspension traces onto components and factors channel outputs and quiescence through the component that owns the channel.Source: A Appendix: Formal Proofs · pp. 23–24
  • The proof shows that if each component conforms, their composition satisfies m-ioco under the composed timeout bound vector.It uses uniformity to realize each specification trace and its admissible next action in the lifted composition.Source: A Appendix: Formal Proofs · p. 24
  • The timed-conformance composition corollary assumes disjoint outputs and shared inputs, then uses input-enabledness and lifting to make m-tioco well-typed before applying Theorem 1.Parallel composition preserves input-enabledness because shared inputs are enabled in every state of both components.Source: A Appendix: Formal Proofs · pp. 24–25
Loading 2609.17640v1…