×

zbMATH — the first resource for mathematics

Bounded determinization of timed automata with silent transitions. (English) Zbl 1425.68216
Summary: Deterministic timed automata are strictly less expressive than their non-deterministic counterparts, which are again less expressive than those with silent transitions. As a consequence, timed automata are in general non-determinizable. This is unfortunate since deterministic automata play a major role in model-based testing, observability and implementability. However, by bounding the length of the traces in the automaton, effective determinization becomes possible. We propose a novel procedure for bounded determinization of timed automata. The procedure unfolds the automata to bounded trees, removes all silent transitions and determinizes via disjunction of guards. The proposed algorithms are optimized to the bounded setting and thus are more efficient and can handle a larger class of timed automata than the general algorithms. We show how to apply the approach in a fault-based test-case generation method, called model-based mutation testing, that was previously restricted to deterministic timed automata. The approach is implemented in a prototype tool and evaluated on several scientific examples and one industrial case study. To our best knowledge, this is the first implementation of this type of procedure for timed automata.
MSC:
68Q45 Formal languages and automata
Software:
IF-2.0; Kronos; Uppaal; z3
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aichernig BK, Lorber F, Ničković D (2013) Time for mutants—model-based mutation testing with timed automata. In: Tests and proofs—7th international conference, TAP 2013, Budapest, Hungary, June 16-20, 2013. Proceedings, pp 20-38
[2] Aichernig BK, Lorber F, Tappler M (2016) Conformance checking of real-time models—symbolic execution vs. bounded model checking. In: Ábrahám E, Bonsangue MM, Johnsen EB (eds) Theory and practice of formal methods—essays dedicated to Frank de Boer on the occasion of his 60th birthday. Lecture Notes in Computer Science, vol 9660. Springer, pp 15-32 · Zbl 1185.68401
[3] Alur, R; Dill, DL, A theory of timed automata, Theoret Comput Sci, 126, 183-235, (1994) · Zbl 0803.68071
[4] Baier, C; Bertrand, N; Bouyer, P; Brihaye, T; Susanne, A (ed.); Alberto, M-S (ed.); Yossi, M (ed.); Sotiris, N (ed.); Wolfgang, T (ed.), When are timed automata determinizable?, 43-54, (2009), Berlin Heidelberg · Zbl 1248.68284
[5] Bengtsson J, Larsen K, Larsson F, Pettersson P, Yi W (1996) UPPAAL a tool suite for automatic verification of real-time systems. In: Alur R, Henzinger TA, Sontag ED (eds) Hybrid systems III. Lecture Notes in Computer Science, vol 1066. Springer, Berlin, Heidelberg, pp 232-243
[6] Bérard, B; Petit, A; Diekert, V; Gastin, P, Characterization of the expressive power of silent transitions in timed automata, Fundamenta Informaticae, 36, 145-182, (1998) · Zbl 0930.68077
[7] Bertrand N, Jéron T, Stainer A, Krichen M (2011) Off-line test selection with test purposes for non-deterministic timed automata. In Abdulla PA, Leino KRM (eds) Tools and algorithms for the construction and analysis of systems. Lecture Notes in Computer Science, vol 6605. Springer, Berlin, Heidelberg, pp 96-111 · Zbl 1315.68082
[8] Biere, A; Cimatti, A; Clarke, EM; Strichman, O; Zhu, Y, No article title, Bounded model checking. Adv Comput, 58, 117-148, (2003)
[9] Bouyer, P; Laroussinie, F; Reynier, P-A; Paul, P (ed.); Wang, Y (ed.), Diagonal constraints in timed automata: forward analysis of timed systems, 112-126, (2005), Berlin, Heidelberg · Zbl 1175.68256
[10] Bozga M, Graf S, Mounier L (2002) If-2.0: a validation environment for component-based real-time systems. In: Brinksma E, Larsen KG (eds) Computer aided verification. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg, pp 343-348 · Zbl 1010.68751
[11] Daws C, Olivero A, Tripakis S, Yovine S (1996) The tool Kronos. In: Alur R, Henzinger TA, Sontag ED (eds) Hybrid systems III. Lecture Notes in Computer Science, vol 1066. Springer, Berlin, Heidelberg, pp 208-219
[12] De Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Proceedings of the theory and practice of software, 14th international conference on tools and algorithms for the construction and analysis of systems, TACAS’08/ETAPS’08. Springer, pp 337-340 · Zbl 1180.68072
[13] Diekert V, Gastin P, Petit A (1997) Removing epsilon-transitions in timed automata. In: Reischuk R, Morvan M (eds) Proceedings of the 14th annual symposium on theoretical aspects of computer science. Lecture Notes in Computer Science, vol 1200. Springer, pp 583-594
[14] Finkel O (2006) Undecidable problems about timed automata. In: Proceedings of the 4th international conference on formal modeling and analysis of timed systems, FORMATS’06. Springer, pp 187-199
[15] Hessel A, Pettersson P (2007) Cover-a test-case generation tool for timed systems. Testing of software and communicating systems, pp 31-34 · Zbl 0930.68077
[16] Hofmann M (ed) (2011) A game approach to determinize timed automata. Springer, Berlin, Heidelberg · Zbl 1326.68173
[17] Kim JH, Larsen KG, Nielsen B, Mikucionis M, Olsen P (2015) Formal analysis and testing of real-time automotive systems using UPPAAL tools. In: Núñez M, Güdemann M (eds) Formal methods for industrial critical systems. Lecture Notes in Computer Science, vol 9128. Springer International Publishing, pp 47-61 · Zbl 1175.68256
[18] Krichen, M; Tripakis, S, Conformance testing for real-time systems, Form Methods Syst Des, 34, 238-304, (2009) · Zbl 1180.68072
[19] Larsen, KG; Pettersson, P; Yi, W, UPPAAL in a nutshell, Softw Tools Technol Transf, 1, 134-152, (1997) · Zbl 1060.68577
[20] Lorber F, Rosenmann A, Nickovic D, Aichernig BK (2015) Bounded determinization of timed automata with silent transitions. In Sankaranarayanan S, Vicario E (eds) Formal modeling and analysis of timed systems—13th international conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings. Lecture Notes in Computer Science, vol 9268. Springer, pp 288-304 · Zbl 06481836
[21] Mikucionis M, Nielsen B, Larsen KG (2003) Real-time system testing on-the-fly. In: Sere K, Waldén M (eds) The 15th nordic workshop on programming theory, number 34 in B. Abo Akademi, Department of Computer Science, Finland, October 29-31. Abstracts, pp 36-38
[22] Schmaltz J, Tretmans J (2008) On conformance testing for timed systems. In: Proceedings of the 6th international conference on formal modeling and analysis of timed systems, FORMATS ’08. Springer, pp 250-264 · Zbl 1171.68556
[23] Tretmans, J; Margaria, T (ed.); Steffen, B (ed.), Test generation with inputs, outputs, and quiescence, 127-146, (1996), Berlin, Heidelberg
[24] Tretmans J (2008) Model based testing with labelled transition systems. In: Formal methods and testing, pp 1-38 · Zbl 1175.68256
[25] Tripakis, S, Folk theorems on the determinization and minimization of timed automata, Inf Process Lett, 99, 222-226, (2006) · Zbl 1185.68401
[26] Wang F (2003) Efficient verification of timed automata with BDD-like data-structures. In: Zuck LD, Attie PC, Cortesi A, Mukhopadhyay S (eds) Verification, model checking, and abstract interpretation. Lecture Notes in Computer Science, vol 2575. Springer Berlin, Heidelberg, pp 189-205 · Zbl 1022.68586
[27] Wang, T; Sun, J; Liu, Y; Wang, X; Li, S; Ábrahám, E (ed.); Havelund, K (ed.), Are timed automata bad for a specification language? language inclusion checking for timed automata, 310-325, (2014), Berlin, Heidelberg
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.