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.
This work is partially supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST and by the ANR national research program PACS (ANR-14-CE28-0002).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
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).
- 2.
This does not necessarily mean that both TAs have the same language, but that the tests did not exhibit any discrepancy.
- 3.
This procedure transforms the word to a non-parametric TA; we nevertheless use the name \(\textsf {TW2PTA}\) for consistency with [11].
- 4.
Note that it does not make sense to measure the syntactical distance, as the structure of the oracle is different.
References
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_4
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.004
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
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-8
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-4
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-0
André, É., Arcaini, P., Gargantini, A., Radavelli, M.: Repairing timed automata clock guards through abstraction and testing. ar**v: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/S0129054109006905
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_6
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
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_2
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-6
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.045
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_3
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.008
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
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-1
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.2357445
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.57
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.028
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
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
Schrijver, A.: Theory of Linear and Integer Programming. Wiley-Interscience Series in Discrete Mathematics and Optimization. Wiley, New York (1999)
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-6
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_21
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
André, É., Arcaini, P., Gargantini, A., Radavelli, M. (2019). Repairing Timed Automata Clock Guards through Abstraction and Testing. In: Beyer, D., Keller, C. (eds) Tests and Proofs. TAP 2019. Lecture Notes in Computer Science(), vol 11823. Springer, Cham. https://doi.org/10.1007/978-3-030-31157-5_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-31157-5_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-31156-8
Online ISBN: 978-3-030-31157-5
eBook Packages: Computer ScienceComputer Science (R0)