nach oben

Formal Methods in System Design

Erschienen in:

09.01.2023

Control strategies for off-line testing of timed systems

verfasst von: Léo Henry, Thierry Jéron, Nicolas Markey

Erschienen in: Formal Methods in System Design | Ausgabe 2/2022

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Partial observability and controllability are two well-known issues in test-case synthesis for reactive systems. We address the problem of partial control in the synthesis of test cases from timed-automata specifications. We extend a previous approach to this problem from the untimed to the timed setting. This extension requires a deep reworking of the models, game interpretation and test-synthesis algorithms. We exhibit strategies of a game that try to minimize both cooperations of the system and distance to the satisfaction of a test purpose or to the next cooperation, and prove they are winning under some fairness assumptions. This entails that when turning those strategies into test cases, we get properties such as soundness and exhaustiveness of the test synthesis method. We finally propose a symbolic algorithm to compute those strategies.

Vorheriger Artikel Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking

Nächster Artikel LTL model checking of self modifying code

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

“Program testing can be used to show the presence of bugs, but never to show their absence!” (Edsger W. Dijkstra)

For this and the following definitions, we may omit to mention superscripts when the corresponding automaton is clear from the context.

This definition is valid because Condition 2 in Def. 5 ensures that guards cannot distinguish between valuations in a given region. Hence the enabled transitions are the same.

Observe that writing \(\textit{reg} \xrightarrow {t}\textit{reg} '\) for a delay \(t \) is execution-specific, as that delay may lead to a region \(\textit{reg} ''\ne \textit{reg} '\) from some configurations in \(\textit{reg} \).

The determinization procedure in [16] also realizes the closure.

The sequence \((W_i^j)_i\) is non-decreasing, and can be computed in terms of clock regions; hence the limit exists and is reached in a finite number of iterations [31].

Notice that if no harmful uncontrollable action exists even after the one leading to \(W^j_\infty \), then \(\textsf {ftPred} (S ')\) captures the behaviour and there is no control loss

In this expression, \({\mathop {\exists }\limits ^{{\infty }}}i\in {\mathbb {N}}, \ \phi (i)\) means that \(\phi (i)\) is true for infinitely many integers. In the same way, \({\mathop {\forall }\limits ^{\infty }}i\in {\mathbb {N}}\ \phi (i)\) means that \(\phi (i)\) is true for all but finitely many integers.

See definitions of \(\textsf {enab} \), \(\textsf {next} \), \(\textsf {SucTemp} \) in Sect. 2.2.

To be perfectly precise, the fairness should depend on the strategy played by the tester to only restrict when the strategy tries to play a controllable action and not when it exists. We hide this dependency for the sake of simplicity but do not use the extra strength of the fairness in our results.

The specific order of computation of the transitions does not impact termination or correctness, but can be of great importance for efficiency.

It corresponds notably to the case where this transition is not triggered by a backpropagation call.

The maximal rank may evolve during the algorithm execution as ranks are added to or removed from \(\textit{active} \).

Tretmans J (1996) Conformance testing with labelled transition systems: Implementation relations and test generation. Comput Netw ISDN Syst 29(1):49–79CrossRef

Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183–235MathSciNetCrossRefMATH

Krichen Moez, Tripakis Stavros (2004) Black-box conformance testing for real-time systems. In Susanne Graf and Laurent Mounier, editors, In: International workshop on model checking software (SPIN2004), number 2989 in Lecture notes in computer science, pages 109–126, Berlin, Heidelberg. Springer Berlin Heidelberg

Krichen M, Tripakis S (2009) Conformance testing for real-time systems. Form Methods Syst Des 34(3):238–304CrossRefMATH

Springintveld J, Vaandrager F, D’Argenio PR (2001) Testing timed automata. Theor Comput Sci 254(1–2):225–257MathSciNetCrossRefMATH

Kaynar Dilsun, Lynch Nancy, Segala Roberto, Vaandrager Frits (2003) Timed I/O automata: A mathematical framework for modeling and analyzing real-time systems. In: Real-time systems symposium, pages 166–177

Kim Guldstrand Larsen, Marius Mikučionis, and Brian Nielsen. (September 2004) Online testing of real-time systems using Uppaal. In Jens Grabowski and Brian Nielsen, (eds), In: Proceedings of the 4th international workshop on formal approaches to software testing (FATES’04), volume 3395 of Lecture notes in computer science, pages 79–94. Springer-Verlag

Bertrand Nathalie, Jéron Thierry, Stainer Amélie, Krichen Moez (2012) Off-line test selection with test purposes for non-deterministic timed automata. Log Methods Comput Sci 8(4):1–33

Cardell-Oliver Rachel, Glover Tim (September 1998) A practical and complete algorithm for testing real-time systems. In: Proceedings of the 5th formal techniques in real-time and fault-tolerant systems (FTRTFT’98), volume 1486 of Lecture Notes in Computer Science, pages 251–261. Springer-Verlag

10.

Castanet Richard, Koné Ousmane, Laurençot Patrice (October 1998) On-the-fly test generation for real time protocols. In: Proceedings of the international conference on computer communications and networks (ICCCN’98), pp 378–387. IEEE Comp. Soc. Press

11.

En-Nouaary A, Dssouli R, Khendek F (2002) Timed WP-method: testing real-time systems. IEEE Trans Softw Eng 28(11):1023–1038CrossRef

12.

Nielsen B, Skou A (2003) Automated test generation from timed automata. Int J Softw Tools Technol Transf 5(1):59–77CrossRefMATH

13.

Briones Laura Brandán, Brinksma Ed (September 2004) A test generation framework for quiescent real-time systems. In Jens Grabowski and Brian Nielsen, (eds), In: Proceedings of the 4th international workshop on formal approaches to software testing (FATES’04), volume 3395 of Lecture Notes in Computer Science, pages 64–78. Springer-Verlag

14.

Tripakis Stavros (2004) Folk theorems on the determinization and minimization of timed automata. In Kim Guldstrand Larsen and Peter Niebert, (eds), In: International conferences on formal modelling and analysis of timed systems (FORMATS’03), volume 2791 of Lecture notes in computer science, pages 182–188, Berlin, Heidelberg. Springer-Verlag

15.

Finkel Olivier (September 2006) Undecidable problems about timed automata. In Eugene Asarin and Patricia Bouyer, (eds), In: International conferences on formal modelling and analysis of timed systems (FORMATS’06), volume 4202 of Lecture notes in computer science, pages 187–199. Springer-Verlag

16.

Bertrand N, Stainer A, Jéron T, Krichen M (2015) A game approach to determinize timed automata. Form Methods Syst Des 46(1):42–80CrossRefMATH

17.

Alur Rajeev, Fix Limor, Henzinger Thomas A (1994) A determinizable class of timed automata. In: International conference on computer aided verification, number 818 in Lecture Notes in Computer Science, pages 1–13. Springer

18.

Asarin E, Maler O, Pnueli A, Sifakis J (1998) Controller synthesis for timed automata. IFAC Proc Vol 31(18):447–452CrossRef

19.

Vijay Suman P, Pandya Paritosh K, Narayanan Krishna Shankara, Manasa Lakshmi (2008) Timed automata with integer resets: Language inclusion and expressiveness. In: International conference on formal modeling and analysis of timed systems, pp 78–92. Springer

20.

Yannakakis Mihalis (2004) Testing, optimization, and games. In: Proceedings of the 31st international colloquium on automata, languages and programming (ICALP’04), Lecture Notes in Computer Science, pages 28–45. Springer-Verlag

21.

David Alexandre, Larsen Kim G, Li Shuhao, Nielsen Brian (March 2008) A game-theoretic approach to real-time system testing. In: Proceedings of the conference on design, automation and test in Europe (DATE’08), pages 486–491

22.

David Alexandre, Larsen KimG, Li Shuhao, Nielsen Brian (2009) Timed testing under partial observability. In: International conference on software testing verification and validation (ICST09), pages 61–70. IEEE

23.

David Alexandre, Larsen Kim G, Li Shuhao, Nielsen Brian (2008) Cooperative testing of timed systems. In: Proceedings of the 4th workshop on model based testing (MBT’08), volume 220 of Electronic Notes in Theoretical Computer Science, pages 79–92

24.

Ramangalahy Solofo (May 1998) Strategies for comformance testing. Research Report 98-010, Max-Planck Institut für Informatik

25.

Henry Léo, Jéron Thierry, Markey Nicolas (2018) Control strategies for off-line testing of timed systems. In: SPIN 2018 - international symposium on model checking software, pages 171–189, 06

26.

van den Boss Petra (2020) Coverage and Games in Model-Based Testing. PhD thesis, Radboud University Nijmegen

27.

Henry Léo (December 2021) There and back again : formal methods and model learning for real-time systems. PhD thesis, University of Rennes 1, France

28.

Hierons Robert M, Merayo Mercedes G, Núñez Manuel (2016) Controllability through nondeterminism in distributed testing. In: IFIP international conference on testing software and systems, pages 89–105. Springer

29.

Ramadge PJ, Wonham WM (1989) The control of discrete event systems. In: Proceedings of the IEEE Special issue on Dynamics of Discrete Event Systems, 77(1):81–98

30.

Asarin Eugene, Maler Oded, Pnueli Amir, Sifakis Joseph (1998) Controller synthesis for timed automata1. IFAC proceedings volumes, 31(18):447–452. 5th IFAC conference on system structure and control 1998 (SSC’98), Nantes, France, 8-10 July

31.

Cassez Franck, David Alexandre, Fleury Emmanuel, Larsen Kim Guldstrand, Lime Didier (August 2005) Efficient on-the-fly algorithms for the analysis of timed games. In Martín Abadi and Luca de Alfaro, (eds), In: Proceedings of the 16th international conference on concurrency theory (CONCUR’05), volume 3653 of Lecture Notes in Computer Science, pages 66–80. Springer-Verlag

32.

Conrado D, Stavros T (1998) Model checking of real-time reachability properties using abstractions. Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, pp 313–329

33.

Johan B, Wang Y (2004) Timed automata: Semantics, algorithms and tools. In: Desel J, Reisig W, Rozenberg G (eds) Lectures on Concurrency and Petri Nets, vol 2098. Lecture Notes in Computer Science. Springer, Verlag

34.

Miné A (2017) Tutorial on static inference of numeric invariants by abstract interpretation. Found Trends Program Lang 4(3–4):120–372CrossRef

35.

Asarin Eugene, Maler Oded, Pnueli Amir, Sifakis Joseph (July 1998) Controller synthesis for timed automata. In: Proceedings of the 5th IFAC conference on system structure and control (SSC’98), pp 469–474. Elsevier

Titel: Control strategies for off-line testing of timed systems
verfasst von: Léo Henry
Thierry Jéron
Nicolas Markey
Publikationsdatum: 09.01.2023
Verlag: Springer US
Erschienen in: Formal Methods in System Design / Ausgabe 2/2022
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-022-00403-w

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2/2022

Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking

Correction: Parameterized verification of leader/follower systems via first-order temporal logic

Assumption-based Runtime Verification

Specifiable robustness in reactive synthesis

Functional synthesis via input–output separation

LTL model checking of self modifying code

Premium Partner