Top

Published in:

2019 | OriginalPaper | Chapter

Repairing Timed Automata Clock Guards through Abstraction and Testing

Authors : Étienne André, Paolo Arcaini, Angelo Gargantini, Marco Radavelli

Published in: Tests and Proofs

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

Timed automata (TAs) are a widely used formalism to specify systems having temporal requirements. However, exactly specifying the system may be difficult, as the user may not know the exact clock constraints triggering state transitions. In this work, we assume the user already specified a TA, and (s)he wants to validate it against an oracle that can be queried for acceptance. Under the assumption that the user only wrote wrong guard transitions (i.e., the structure of the TA is correct), the search space for the correct TA can be represented by a Parametric Timed Automaton (PTA), i.e., a TA in which some constants are parametrized. The paper presents a process that (i) abstracts the initial (faulty) TA \( ta_{init} \) in a PTA \( pta \); (ii) generates some test data (i.e., timed traces) from \( pta \); (iii) assesses the correct evaluation of the traces with the oracle; (iv) uses the IMITATOR tool for synthesizing some constraints \(\varphi \) on the parameters of \( pta \); (v) instantiate from \(\varphi \) a TA \( ta_{rep} \) as final repaired model. Experiments show that the approach is successfully able to partially repair the initial design of the user.

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 "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

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

previous chapter Learning Communicating State Machines

next chapter Proving a Non-blocking Algorithm for Process Renaming with TLA

To limit the number of tests, we only keep the maximal accepted traces (i.e., we remove accepted traces included in longer accepted traces), and the minimal rejected traces (i.e., we remove rejected traces having as prefix another rejected trace).

This does not necessarily mean that both TAs have the same language, but that the tests did not exhibit any discrepancy.

This procedure transforms the word to a non-parametric TA; we nevertheless use the name \(\textsf {TW2PTA}\) for consistency with [11].

Note that it does not make sense to measure the syntactical distance, as the structure of the oracle is different.

Aichernig, B.K., Hörmaier, K., Lorber, F.: Debugging with timed automata mutations. In: Bondavalli, A., Di Giandomenico, F.D. (eds.) SAFECOMP 2014. LNCS, vol. 8666, pp. 49–64. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10506-2_4CrossRef

Aichernig, B.K., Jöbstl, E., Tiran, S.: Model-based mutation testing via symbolic refinement checking. Sci. Comput. Program. 97(P4), 383–404 (2015). https://doi.org/10.1016/j.scico.2014.05.004CrossRef

Aichernig, B.K., Lorber, F., Ničković, D.: Time for mutants—model-based mutation testing with timed automata. In: Veanes, M., Viganò, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 20–38. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38916-0_2CrossRef

Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8MathSciNetCrossRefMATH

Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. A determinizable classof timed automata. Theoret. Comput. Sci. 211(1–2), 253–273 (1999). https://doi.org/10.1016/S0304-3975(97)00173-4MathSciNetCrossRefMATH

Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Kosaraju, S.R., Johnson, D.S., Aggarwal, A. (eds.) STOC, pp. 592–601. ACM, New York (1993). https://doi.org/10.1145/167088.167242

André, É.: What’s decidable about parametric timed automata? Int. J. Softw. Tools Technol. Transf. 21(2), 203–219 (2019). https://doi.org/10.1007/s10009-017-0467-0CrossRef

André, É., Arcaini, P., Gargantini, A., Radavelli, M.: Repairing timed automata clock guards through abstraction and testing. arXiv:1907.02133 (2019)

André, É., Chatain, T., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. Int. J. Found. Comput. Sci. 20(5), 819–836 (2009). https://doi.org/10.1142/S0129054109006905MathSciNetCrossRefMATH

10.

André, É., Fribourg, L., Kühne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33–36. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_6CrossRef

11.

André, É., Hasuo, I., Waga, M.: Offline timed pattern matching under uncertainty. In: Lin, A.W., Sun, J. (eds.) ICECCS, pp. 10–20. IEEE CPS (2018). https://doi.org/10.1109/ICECCS2018.2018.00010

12.

André, É., Lin, S.-W.: Learning-based compositional parameter synthesis for event-recording automata. In: Bouajjani, A., Silva, A. (eds.) FORTE 2017. LNCS, vol. 10321, pp. 17–32. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-60225-7_2CrossRef

13.

Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987). https://doi.org/10.1016/0890-5401(87)90052-6MathSciNetCrossRefMATH

14.

Arcaini, P., Gargantini, A., Radavelli, M.: Achieving change requirements of feature models by an evolutionary approach. J. Syst. Softw. 150, 64–76 (2019). https://doi.org/10.1016/j.jss.2019.01.045CrossRef

15.

Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27755-2_3CrossRefMATH

16.

Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theoret. Comput. Sci. 411(47), 4029–4054 (2010). https://doi.org/10.1016/j.tcs.2010.07.008MathSciNetCrossRefMATH

17.

Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 77–117. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78917-8_3CrossRef

18.

Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. J. Logic Algebraic Program. 52–53, 183–220 (2002). https://doi.org/10.1016/S1567-8326(02)00037-1MathSciNetCrossRefMATH

19.

Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for real-time systems. IEEE Trans. Softw. Eng. 41(5), 445–461 (2015). https://doi.org/10.1109/TSE.2014.2357445CrossRef

20.

Lin, S.W., André, É., Liu, Y., Sun, J., Dong, J.S.: Learning assumptions for compositional verification of timed systems. Trans. Softw. Eng. 40(2), 137–153 (2014). https://doi.org/10.1109/TSE.2013.57CrossRef

21.

Luthmann, L., Gerecht, T., Stephan, A., Bürdek, J., Lochau, M.: Minimum/maximum delay testing of product lines with unbounded parametric real-time constraints. J. Syst. Softw. 149, 535–553 (2019). https://doi.org/10.1016/j.jss.2018.12.028CrossRef

22.

Papadakis, M., Kintis, M., Zhang, J., Jia, Y., Le Traon, Y., Harman, M.: Mutation testing advances: an analysis and survey. In: Advances in Computers. Elsevier (2018). https://doi.org/10.1016/bs.adcom.2018.03.015

23.

Prud’homme, C., Fages, J.G., Lorca, X.: Choco Documentation. TASC - LS2N CNRS UMR 6241, COSLING S.A.S. (2017). http://www.choco-solver.org

24.

Schrijver, A.: Theory of Linear and Integer Programming. Wiley-Interscience Series in Discrete Mathematics and Optimization. Wiley, New York (1999)MATH

25.

Springintveld, J., Vaandrager, F., D’Argenio, P.R.: Testing timed automata. Theoret. Comput. Sci. 254(1–2), 225–257 (2001). https://doi.org/10.1016/S0304-3975(99)00134-6MathSciNetCrossRefMATH

26.

Wang, T., Sun, J., Liu, Y., Wang, X., Li, S.: Are timed automata bad for a specification language? Language inclusion checking for timed automata. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 310–325. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_21CrossRef

Title: Repairing Timed Automata Clock Guards through Abstraction and Testing
Authors: Étienne André
Paolo Arcaini
Angelo Gargantini
Marco Radavelli
Publisher: Springer International Publishing
Book: Tests and Proofs
Print ISBN: 978-3-030-31156-8

Electronic ISBN: 978-3-030-31157-5

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-31157-5_9

Springer Professional

Abstract

Please log in to get access to your license.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner