Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design
Published in: Formal Methods in System Design 2/2022

09-01-2023

Control strategies for off-line testing of timed systems

Authors: Léo Henry, Thierry Jéron, Nicolas Markey

Published in: Formal Methods in System Design | Issue 2/2022

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.
previous article Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
next article LTL model checking of self modifying code

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Footnotes
1
“Program testing can be used to show the presence of bugs, but never to show their absence!” (Edsger W. Dijkstra)
 
2
For this and the following definitions, we may omit to mention superscripts when the corresponding automaton is clear from the context.
 
3
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.
 
4
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} \).
 
5
The determinization procedure in [16] also realizes the closure.
 
6
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].
 
7
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
 
8
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.
 
9
See definitions of \(\textsf {enab} \), \(\textsf {next} \), \(\textsf {SucTemp} \) in Sect.  2.2.
 
10
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.
 
11
The specific order of computation of the transitions does not impact termination or correctness, but can be of great importance for efficiency.
 
12
It corresponds notably to the case where this transition is not triggered by a backpropagation call.
 
13
The maximal rank may evolve during the algorithm execution as ranks are added to or removed from \(\textit{active} \).
 
Literature
1.
Tretmans J (1996) Conformance testing with labelled transition systems: Implementation relations and test generation. Comput Netw ISDN Syst 29(1):49–79CrossRef
2.
3.
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
4.
Krichen M, Tripakis S (2009) Conformance testing for real-time systems. Form Methods Syst Des 34(3):238–304CrossRefMATH
5.
6.
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
7.
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
8.
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
9.
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
Metadata
Title
Control strategies for off-line testing of timed systems
Authors
Léo Henry
Thierry Jéron
Nicolas Markey
Publication date
09-01-2023
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 2/2022
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-022-00403-w

Other articles of this Issue 2/2022

Formal Methods in System Design 2/2022 Go to the issue

OriginalPaper

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

Correction

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

OriginalPaper

LTL model checking of self modifying code

OriginalPaper

Specifiable robustness in reactive synthesis

OriginalPaper

Assumption-based Runtime Verification

OriginalPaper

Functional synthesis via input–output separation

Premium Partner

    Image Credits