Luthmann, Lars ; Göttmann, Hendrik ; Lochau, Malte (2019)
Compositional Liveness-Preserving Conformance Testing of Timed I/O Automata - Technical Report.
doi: 10.48550/arXiv.1909.03703
Report, Bibliographie
Abstract
I/O 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 real-time 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 real-time 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 I/O Labeled Transition Systems (TIOLTS), a semantic model of Timed I/O 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.
| Item Type: | Report |
|---|---|
| Erschienen: | 2019 |
| Creators: | Luthmann, Lars ; Göttmann, Hendrik ; Lochau, Malte |
| Type of entry: | Bibliographie |
| Title: | Compositional Liveness-Preserving Conformance Testing of Timed I/O Automata - Technical Report |
| Language: | English |
| Date: | 9 September 2019 |
| Publisher: | arXiv |
| Series: | Logic in Computer Science |
| Edition: | 1.Version |
| DOI: | 10.48550/arXiv.1909.03703 |
| URL / URN: | https://arxiv.org/abs/1909.03703 |
| Corresponding Links: | |
| Abstract: | I/O 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 real-time 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 real-time 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 I/O Labeled Transition Systems (TIOLTS), a semantic model of Timed I/O 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. |
| Divisions: | 18 Department of Electrical Engineering and Information Technology 18 Department of Electrical Engineering and Information Technology > Institute of Computer Engineering > Real-Time Systems 18 Department of Electrical Engineering and Information Technology > Institute of Computer Engineering |
| Date Deposited: | 16 Sep 2019 05:53 |
| Last Modified: | 11 Aug 2023 08:08 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum