Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2507.18205 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915408009756672 |
|---|---|
| author | Briones, Laura Brandán Gerhold, Marcus Bos, Petra van den Stoelinga, Mariëlle |
| author_facet | Briones, Laura Brandán Gerhold, Marcus Bos, Petra van den Stoelinga, Mariëlle |
| contents | Model-based testing (MBT) derives test suites from a behavioural specification of the system under test. In practice, engineers favour simple models, such as labelled transition systems (LTSs). However, to deal with quiescence - the absence of observable output - in practice, a time-out needs to be set to conclude observation of quiescence. Timed MBT exists, but it typically relies on the full arsenal of timed automata (TA).
We present a lifting operator $χ^{\scriptstyle M}\!$ that adds timing without the TA overhead: given an LTS, $χ^{\scriptstyle M}\!$ introduces a single clock for a user chosen time bound $M>0$ to declare quiescence. In the timed automaton, the clock is used to model that outputs should happen before the clock reaches value $M$, while quiescence occurs exactly at time $M$. This way we provide a formal basis for the industrial practice of choosing a time-out to conclude quiescence. Our contributions are threefold: (1) an implementation conforms under $\mathbf{ioco}$ if and only if its lifted version conforms under timed $\mathbf{tioco_M}$ (2) applying $χ^{\scriptstyle M}\!$ before or after the standard $\mathbf{ioco}$ test-generation algorithm yields the same set of tests, and (3) the lifted TA test suite and the original LTS test suite deliver identical verdicts for every implementation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_18205 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Time for Quiescence: Modelling quiescent behaviour in testing via time-outs in timed automata Briones, Laura Brandán Gerhold, Marcus Bos, Petra van den Stoelinga, Mariëlle Formal Languages and Automata Theory Model-based testing (MBT) derives test suites from a behavioural specification of the system under test. In practice, engineers favour simple models, such as labelled transition systems (LTSs). However, to deal with quiescence - the absence of observable output - in practice, a time-out needs to be set to conclude observation of quiescence. Timed MBT exists, but it typically relies on the full arsenal of timed automata (TA). We present a lifting operator $χ^{\scriptstyle M}\!$ that adds timing without the TA overhead: given an LTS, $χ^{\scriptstyle M}\!$ introduces a single clock for a user chosen time bound $M>0$ to declare quiescence. In the timed automaton, the clock is used to model that outputs should happen before the clock reaches value $M$, while quiescence occurs exactly at time $M$. This way we provide a formal basis for the industrial practice of choosing a time-out to conclude quiescence. Our contributions are threefold: (1) an implementation conforms under $\mathbf{ioco}$ if and only if its lifted version conforms under timed $\mathbf{tioco_M}$ (2) applying $χ^{\scriptstyle M}\!$ before or after the standard $\mathbf{ioco}$ test-generation algorithm yields the same set of tests, and (3) the lifted TA test suite and the original LTS test suite deliver identical verdicts for every implementation. |
| title | Time for Quiescence: Modelling quiescent behaviour in testing via time-outs in timed automata |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2507.18205 |