Off-line test selection with test purposes for non-deterministic timed automata

DOI10.1007/978-3-642-19835-9_10MaRDI QIDQ3000640zbMATH OpenOpenAlexFDO

Authors Nathalie Bertrand, Thierry Jéron, Amélie Stainer, Moez Krichen

Publication date 19 May 2011

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1207.6267

zbMATH Keywords

timed automatagameconformance testingurgencypartial observabilitytest purposeapproximate determinization

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: 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 first 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 specification. 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.

Recommendations

• Off-line test selection with test purposes for non-deterministic timed automata
• Formal Approaches to Software Testing
• scientific article; zbMATH DE number 1701769
• Testing timed automata
• Control Strategies for Off-Line Testing of Timed Systems

Cites work

• scientific article; zbMATH DE number 2013786 (Why is no real title available?)
• scientific article; zbMATH DE number 938070 (Why is no real title available?)
• scientific article; zbMATH DE number 2209335 (Why is no real title available?)
• A game approach to determinize timed automata
• A theory of timed automata
• Conformance testing for real-time systems
• Folk theorems on the determinization and minimization of timed automata
• Formal Approaches to Software Testing
• Formal Approaches to Software Testing
• Off-line test selection with test purposes for non-deterministic timed automata
• On Conformance Testing for Timed Systems
• On the power of non-observable actions in timed automata
• Timed I/O automata: a complete specification theory for real-time systems
• Undecidable Problems About Timed Automata

Cited in

(6)

• Control Strategies for Off-Line Testing of Timed Systems
• Formal Approaches to Software Testing
• Bounded determinization of timed automata with silent transitions
• Bounded determinization of timed automata with silent transitions
• A game approach to determinize timed automata
• Off-line test selection with test purposes for non-deterministic timed automata

This page was built for publication: Off-line test selection with test purposes for non-deterministic timed automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000640)