Off-line test selection with test purposes for non-deterministic timed automata
This article proposes novel off-line test generation techniques from non-deterministic timed automata with inputs and outputs (TAIOs) in the formal framework of the tioco conformance theory. In this context, a fi?rst problem is the determinization of TAIOs, which is necessary to foresee next enabled...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-10-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1037/pdf |
| _version_ | 1797268680480915456 |
|---|---|
| author | Nathalie Bertrand Thierry Jéron Amélie Stainer Moez Krichen |
| author_facet | Nathalie Bertrand Thierry Jéron Amélie Stainer Moez Krichen |
| author_sort | Nathalie Bertrand |
| collection | DOAJ |
| description | This article proposes novel off-line test generation techniques from
non-deterministic timed automata with inputs and outputs (TAIOs) in the formal
framework of the tioco conformance theory. In this context, a fi?rst problem is
the determinization of TAIOs, which is necessary to foresee next enabled
actions after an observable trace, but is in general impossible because not all
timed automata are determinizable. This problem is solved thanks to an
approximate determinization using a game approach. The algorithm performs an
io-abstraction which preserves the tioco conformance relation and thus
guarantees the soundness of generated test cases. A second problem is the
selection of test cases from a TAIO speci?fication. The selection here relies
on a precise description of timed behaviors to be tested which is carried out
by expressive test purposes modeled by a generalization of TAIOs. Finally, an
algorithm is described which generates test cases in the form of TAIOs equipped
with verdicts, using a symbolic co-reachability analysis guided by the test
purpose. Properties of test cases are then analyzed with respect to the
precision of the approximate determinization: when determinization is exact,
which is the case on known determinizable classes, in addition to soundness,
properties characterizing the adequacy of test cases verdicts are also
guaranteed. |
| first_indexed | 2024-04-25T01:36:20Z |
| format | Article |
| id | doaj.art-246cee29ce85487fb4514a6c3dd73ce6 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:20Z |
| publishDate | 2012-10-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-246cee29ce85487fb4514a6c3dd73ce62024-03-08T09:28:03ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-10-01Volume 8, Issue 410.2168/LMCS-8(4:8)20121037Off-line test selection with test purposes for non-deterministic timed automataNathalie Bertrandhttps://orcid.org/0000-0002-9957-5394Thierry Jéronhttps://orcid.org/0000-0002-9922-6186Amélie StainerMoez KrichenThis article proposes novel off-line test generation techniques from non-deterministic timed automata with inputs and outputs (TAIOs) in the formal framework of the tioco conformance theory. In this context, a fi?rst problem is the determinization of TAIOs, which is necessary to foresee next enabled actions after an observable trace, but is in general impossible because not all timed automata are determinizable. This problem is solved thanks to an approximate determinization using a game approach. The algorithm performs an io-abstraction which preserves the tioco conformance relation and thus guarantees the soundness of generated test cases. A second problem is the selection of test cases from a TAIO speci?fication. The selection here relies on a precise description of timed behaviors to be tested which is carried out by expressive test purposes modeled by a generalization of TAIOs. Finally, an algorithm is described which generates test cases in the form of TAIOs equipped with verdicts, using a symbolic co-reachability analysis guided by the test purpose. Properties of test cases are then analyzed with respect to the precision of the approximate determinization: when determinization is exact, which is the case on known determinizable classes, in addition to soundness, properties characterizing the adequacy of test cases verdicts are also guaranteed.https://lmcs.episciences.org/1037/pdfcomputer science - formal languages and automata theoryd.2.4d.2.5d.4.7f.1.1 |
| spellingShingle | Nathalie Bertrand Thierry Jéron Amélie Stainer Moez Krichen Off-line test selection with test purposes for non-deterministic timed automata Logical Methods in Computer Science computer science - formal languages and automata theory d.2.4 d.2.5 d.4.7 f.1.1 |
| title | Off-line test selection with test purposes for non-deterministic timed automata |
| title_full | Off-line test selection with test purposes for non-deterministic timed automata |
| title_fullStr | Off-line test selection with test purposes for non-deterministic timed automata |
| title_full_unstemmed | Off-line test selection with test purposes for non-deterministic timed automata |
| title_short | Off-line test selection with test purposes for non-deterministic timed automata |
| title_sort | off line test selection with test purposes for non deterministic timed automata |
| topic | computer science - formal languages and automata theory d.2.4 d.2.5 d.4.7 f.1.1 |
| url | https://lmcs.episciences.org/1037/pdf |
| work_keys_str_mv | AT nathaliebertrand offlinetestselectionwithtestpurposesfornondeterministictimedautomata AT thierryjeron offlinetestselectionwithtestpurposesfornondeterministictimedautomata AT ameliestainer offlinetestselectionwithtestpurposesfornondeterministictimedautomata AT moezkrichen offlinetestselectionwithtestpurposesfornondeterministictimedautomata |