Skip to main content
SpringerLink
Log in

Time to Learn – Learning Timed Automata from Tests

  • Conference paper
  • First Online:
Formal Modeling and Analysis of Timed Systems (FORMATS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11750))

Abstract

Model learning has gained increasing interest in recent years. It derives behavioural models from test data of black-box systems. The main advantage offered by such techniques is that they enable model-based analysis without access to the internals of a system. Applications range from fully automated testing over model checking to system understanding. Current work focuses on learning variations of finite state machines. However, most techniques consider discrete time. In this paper, we present a novel method for learning timed automata, finite state machines extended with real-valued clocks. The learning method generates a model consistent with a set of timed traces collected via testing. This generation is based on genetic programming, a search-based technique for automatic program creation. We evaluate our approach on \(\mathbf {44}\) timed systems, comprised of four systems from the literature (two industrial and two academic) and \(\mathbf {40}\) randomly generated examples.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Abdessalem, R.B., Nejati, S., Briand, L.C., Stifter, T.: Testing vision-based control systems using learnable evolutionary algorithms. In: ICSE 2018, pp. 1016–1026. ACM (2018). https://doi.org/10.1145/3180155.3180160

  2. Aichernig, B.K., et al.: Model-based mutation testing of an industrial measurement device. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 1–19. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09099-3_1

    Chapter  Google Scholar 

  3. 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_2

    Chapter  Google Scholar 

  4. Aichernig, B.K., Mostowski, W., Mousavi, M.R., Tappler, M., Taromirad, M.: Model learning and model-based testing. In: Bennaceur, A., Hähnle, R., Meinke, K. (eds.) Machine Learning for Dynamic Software Analysis: Potentials and Limits. LNCS, vol. 11026, pp. 74–100. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96562-8_3

    Chapter  Google Scholar 

  5. Aichernig, B.K., Tappler, M.: Efficient active automata learning via mutation testing. J. Autom. Reason. (2018). https://doi.org/10.1007/s10817-018-9486-0

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

    Article  MathSciNet  MATH  Google Scholar 

  7. Argyros, G., Stais, I., Jana, S., Keromytis, A.D., Kiayias, A.: SFADiff: automated evasion attacks and fingerprinting using black-box differential automata learning. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 1690–1701. ACM (2016). https://doi.org/10.1145/2976749.2978383

  8. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7

    Chapter  Google Scholar 

  9. Bornot, S., Sifakis, J., Tripakis, S.: Modeling urgency in timed systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 103–129. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-49213-5_5

    Chapter  Google Scholar 

  10. David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: Johansson, K.H., Yi, W. (eds.) HSCC 2010, pp. 91–100. ACM (2010). https://doi.org/10.1145/1755952.1755967

  11. Elkind, E., Genest, B., Peled, D., Qu, H.: Grey-box checking. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 420–435. Springer, Heidelberg (2006). https://doi.org/10.1007/11888116_30

    Chapter  Google Scholar 

  12. Fiterău-Broştean, P., Janssen, R., Vaandrager, F.: Combining model learning and model checking to analyze TCP implementations. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 454–471. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_25

    Chapter  Google Scholar 

  13. Fraser, G., Arcuri, A.: EvoSuite: automatic test suite generation for object-oriented software. In: SIGSOFT/FSE 2011, pp. 416–419. ACM (2011). https://doi.org/10.1145/2025113.2025179

  14. Gómez, R.: A compositional translation of timed automata with deadlines to Uppaal timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 179–194. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04368-0_15

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  16. Grinchtein, O., Jonsson, B., Pettersson, P.: Inference of event-recording automata using timed decision trees. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 435–449. Springer, Heidelberg (2006). https://doi.org/10.1007/11817949_29

    Chapter  Google Scholar 

  17. Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 357–370. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46002-0_25

    Chapter  Google Scholar 

  18. 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_3

    Chapter  Google Scholar 

  19. Hessel, A., Larsen, K.G., Nielsen, B., Pettersson, P., Skou, A.: Time-optimal real-time test case generation using Uppaal. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 114–130. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24617-6_9

    Chapter  Google Scholar 

  20. de la Higuera, C.: Grammatical Inference: Learning Automata and Grammars. Cambridge University Press, New York (2010)

    Book  Google Scholar 

  21. Hungar, H., Margaria, T., Steffen, B.: Test-based model generation for legacy systems. In: ITC 2003, pp. 971–980. IEEE (2003). https://doi.org/10.1109/TEST.2003.1271084

  22. Isberner, M., Howar, F., Steffen, B.: The open-source LearnLib - a framework for active automata learning. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 487–495. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_32

    Chapter  Google Scholar 

  23. Johnson, C.G.: Genetic programming with fitness based on model checking. In: Ebner, M., O’Neill, M., Ekárt, A., Vanneschi, L., Esparcia-Alcázar, A.I. (eds.) EuroGP 2007. LNCS, vol. 4445, pp. 114–124. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71605-1_11

    Chapter  Google Scholar 

  24. Katz, G., Peled, D.: Synthesizing, correcting and improving code, using model checking-based genetic programming. STTT 19(4), 449–464 (2017). https://doi.org/10.1007/s10009-016-0418-1

    Article  Google Scholar 

  25. Koza, J.R.: Genetic Programming - On the Programming of Computers by Means of Natural Selection. Complex adaptive systems. MIT Press, Cambridge (1993)

    MATH  Google Scholar 

  26. Lai, Z., Cheung, S.C., Jiang, Y.: Dynamic model learning using genetic algorithm under adaptive model checking framework. In: QSIC 2006, pp. 410–417. IEEE (2006). https://doi.org/10.1109/QSIC.2006.25

  27. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1–2), 134–152 (1997). https://doi.org/10.1007/s100090050010

    Article  Google Scholar 

  28. Lefticaru, R., Ipate, F., Tudose, C.: Automated model design using genetic algorithms and model checking. In: BCI 2009, pp. 79–84. IEEE (2009). https://doi.org/10.1109/BCI.2009.15

  29. Lin, S.-W., André, É., Dong, J.S., Sun, J., Liu, Y.: An efficient algorithm for learning event-recording automata. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 463–472. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24372-1_35

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  31. Lucas, S.M., Reynolds, T.J.: Learning DFA: evolution versus evidence driven state merging. In: CEC 2003, pp. 351–358. IEEE (2003). https://doi.org/10.1109/CEC.2003.1299597

  32. Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning deterministic probabilistic automata from a model checking perspective. Mach. Learn. 105(2), 255–299 (2016). https://doi.org/10.1007/s10994-016-5565-9

    Article  MathSciNet  MATH  Google Scholar 

  33. de Matos Pedro, A., Crocker, P.A., de Sousa, S.M.: Learning stochastic timed automata from sample executions. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 508–523. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34026-0_38

    Chapter  Google Scholar 

  34. Mediouni, B.L., Nouri, A., Bozga, M., Bensalem, S.: Improved learning for stochastic timed models by state-merging algorithms. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 178–193. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_13

    Chapter  Google Scholar 

  35. Mitchell, M.: An Introduction to Genetic Algorithms. MIT Press, Cambridge (1998)

    MATH  Google Scholar 

  36. Nenzi, L., Silvetti, S., Bartocci, E., Bortolussi, L.: A robust genetic algorithm for learning temporal specifications from data. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 323–338. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99154-2_20

    Chapter  Google Scholar 

  37. Nowostawski, M., Poli, R.: Parallel genetic algorithm taxonomy. In: KES 1999, pp. 88–92. IEEE (1999). https://doi.org/10.1109/KES.1999.820127

  38. Pastore, F., Micucci, D., Mariani, L.: Timed k-tail: automatic inference of timed automata. In: ICST 2017, pp. 401–411 (2017). https://doi.org/10.1109/ICST.2017.43

  39. Peled, D.A., Vardi, M.Y., Yannakakis, M.: Black box checking. JALC 7(2), 225–246 (2002)

    MathSciNet  MATH  Google Scholar 

  40. de Ruiter, J., Poll, E.: Protocol state fuzzing of TLS implementations. In: USENIX Security 2015, pp. 193–206. USENIX Association (2015). https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/de-ruiter

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

    Article  MathSciNet  MATH  Google Scholar 

  42. Steffen, B., Howar, F., Merten, M.: Introduction to active automata learning from a practical perspective. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 256–296. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21455-4_8

    Chapter  Google Scholar 

  43. Tappler, M., Aichernig, B.K., Bloem, R.: Model-based testing IoT communication via active automata learning. In: ICST 2017, pp. 276–287 (2017). https://doi.org/10.1109/ICST.2017.32

  44. Tappler, M., Aichernig, B.K., Larsen, K.G., Lorber, F.: Learning timed automata via genetic programming. CoRR abs/1808.07744 (2018). http://arxiv.org/abs/1808.07744

  45. Tappler, M., Pferscher, A.: Supplementary Material for “Learning Timed Automata via Genetic Programming” (2019). https://doi.org/10.6084/m9.figshare.5513575.v1. https://figshare.com/articles/Supplementary_Material_for_Learning_Timed_Automata_via_Genetic_Programming_/5513575

  46. Verwer, S., De Weerdt, M., Witteveen, C.: An algorithm for learning real-time automata. In: Benelearn 2007 (2007)

    Google Scholar 

  47. Verwer, S., de Weerdt, M., Witteveen, C.: A likelihood-ratio test for identifying probabilistic deterministic real-time automata from positive data. In: Sempere, J.M., García, P. (eds.) ICGI 2010. LNCS (LNAI), vol. 6339, pp. 203–216. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15488-1_17

    Chapter  Google Scholar 

  48. Walkinshaw, N., Derrick, J., Guo, Q.: Iterative refinement of reverse-engineered models by model-based testing. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 305–320. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-05089-3_20

    Chapter  Google Scholar 

  49. Walkinshaw, N., Fraser, G.: Uncertainty-driven black-box test data generation. In: ICST 2017, pp. 253–263 (2017). https://doi.org/10.1109/ICST.2017.30

Download references

Acknowledgment

The work of B. Aichernig and M. Tappler has been carried out as part of the TU Graz LEAD project “Dependable Internet of Things in Adverse Environments”. The work of K. Larsen and F. Lorber has been conducted within the ENABLE-S3 project that has received funding from the ECSEL Joint Undertaking under grant agreement no. 692455. This joint undertaking receives support from the European Union’s Horizon 2020 research and innovation programme and Austria, Denmark, Germany, Finland, Czech Republic, Italy, Spain, Portugal, Poland, Ireland, Belgium, France, Netherlands, United Kingdom, Slovakia, Norway. We would like to thank student Andrea Pferscher for her help in implementing the demonstrator. We also want to thank the anonymous reviewers for their insightful comments and suggestions.

Author information

Authors and Affiliations

  1. Institute of Software Technology, Graz University of Technology, Graz, Austria

    Martin Tappler & Bernhard K. Aichernig

  2. Department of Computer Science, Aalborg University, Aalborg, Denmark

    Kim Guldstrand Larsen & Florian Lorber

Authors
  1. Martin Tappler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernhard K. Aichernig
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kim Guldstrand Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Florian Lorber
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martin Tappler .

Editor information

Editors and Affiliations

  1. Université Paris 13, Villetaneuse, France

    Étienne André

  2. University of Twente, Enschede, The Netherlands

    Mariëlle Stoelinga

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Tappler, M., Aichernig, B.K., Larsen, K.G., Lorber, F. (2019). Time to Learn – Learning Timed Automata from Tests. In: André, É., Stoelinga, M. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2019. Lecture Notes in Computer Science(), vol 11750. Springer, Cham. https://doi.org/10.1007/978-3-030-29662-9_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29662-9_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29661-2

  • Online ISBN: 978-3-030-29662-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation