Abstract
Checking the language inclusion between two models is a fundamental problem arising in application areas such as formal verification or refinement in top-down design. We propose an incremental procedure for checking the language inclusion between two real-time specifications, modeled as networks of deterministic timed automata, where the two specifications are equivalent up to one component. For such classes of systems we aim to improve the efficiency of the language inclusion check by exploiting the compositional nature of the problem and avoiding the explicit parallel composition of the timed automata in the network. We first develop a generic procedure that gives freedom to specific implementation choices. We then propose an instantiation of the procedure that is based on bounded model checking techniques. We illustrate the application of our approach in a case study and discuss promising experimental results.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aichernig, B.K., Brandl, H., Jöbstl, E., Krenn, W.: Uml in action: a two-layered interpretation for testing. ACM SIGSOFT Software Engineering Notes 36(1), 1–8 (2011)
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)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Alur, R., Itai, A., Kurshan, R.P., Yannakakis, M.: Timing verification by successive approximation. Inf. Comput. 118(1), 142–157 (1995)
Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded model checking for timed systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 243–259. Springer, Heidelberg (2002)
Badban, B., Lange, M.: Exact incremental analysis of timed automata with an SMT-solver. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 177–192. Springer, Heidelberg (2011)
Brillout, A., He, N., Mazzucchi, M., Kroening, D., Purandare, M., Rümmer, P., Weissenbacher, G.: Mutation-based test case generation for simulink models. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 208–227. Springer, Heidelberg (2010)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
He, N., Rümmer, P., Kroening, D.: Test-case generation for embedded simulink via formal concept analysis. In: DAC, pp. 224–229 (2011)
Krichen, M., Tripakis, S.: Conformance testing for real-time systems. Formal Methods in System Design 34(3), 238–304 (2009)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1(1-2), 134–152 (1997)
Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of timed automata via satisfiability checking. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 225–244. Springer, Heidelberg (2002)
Schlick, R., Herzner, W., Jöbstl, E.: Fault-based generation of test cases from UML-models – approach and some experiences. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 270–283. Springer, Heidelberg (2011)
Steiner, W.: An evaluation of smt-based schedule synthesis for time-triggered multi-hop networks. In: RTSS, pp. 375–384 (2010)
Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008)
van der Bijl, M., Rensink, A., Tretmans, J.: Compositional testing with ioco. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 86–100. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Krenn, W., Ničković, D., Tec, L. (2013). Incremental Language Inclusion Checking for Networks of Timed Automata. In: Braberman, V., Fribourg, L. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2013. Lecture Notes in Computer Science, vol 8053. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40229-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-40229-6_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40228-9
Online ISBN: 978-3-642-40229-6
eBook Packages: Computer ScienceComputer Science (R0)