Abstract
Quasi-equal clock reduction for networks of timed automata replaces equivalence classes of clocks which are equal except for unstable phases, i.e., points in time where these clocks differ on their valuation, by a single representative clock. An existing approach yields significant reductions of the overall verification time but is limited to so-called well-formed networks and local queries, i.e., queries which refer to a single timed automaton only. In this work we present two new transformations. The first, for networks of timed automata, summarises unstable phases without losing information under weaker well-formedness assumptions than needed by the existing approach. The second, for queries, now supports the full query language of Uppaal. We demonstrate that the cost of verifying non-local properties is much lower in transformed networks than in their original counterparts with quasi-equal clocks.
Chapter PDF
Similar content being viewed by others
References
Rappaport, T.S.: Wireless communications, vol. 2. Prentice Hall (2002)
Cena, G., Seno, L., et al.: Performance analysis of ethernet powerlink networks for distributed control and automation systems. CSI 31(3), 566–572 (2009)
Alur, R., Dill, D.: A theory of timed automata. TCS 126(2), 183–235 (1994)
Herrera, C., Westphal, B., Feo-Arenis, S., Muñiz, M., Podelski, A.: Reducing quasi-equal clocks in networks of timed automata. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 155–170. Springer, Heidelberg (2012)
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)
Limal, S., Potier, S., Denis, B., Lesage, J.: Formal verification of redundant media extension of ethernet powerlink. In: ETFA, pp. 1045–1052. IEEE (2007)
Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: RTSS, pp. 73–81. IEEE (1996)
Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998)
André, É.: Dynamic clock elimination in parametric timed automata. In: FSFMA, OASICS, pp. 18–31, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)
Braberman, V., Garbervestky, D., Kicillof, N., Monteverde, D., Olivero, A.: Speeding up model checking of timed-models by combining scenario specialization and live component analysis. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 58–72. Springer, Heidelberg (2009)
Braberman, V.A., Garbervetsky, D., Olivero, A.: Improving the verification of timed systems using influence information. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 21–36. Springer, Heidelberg (2002)
Muñiz, M., Westphal, B., Podelski, A.: Timed automata with disjoint activity. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 188–203. Springer, Heidelberg (2012)
Balaguer, S., Chatain, T.: Avoiding shared clocks in networks of timed automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 100–114. Springer, Heidelberg (2012)
Muñiz, M., Westphal, B., Podelski, A.: Detecting quasi-equal clocks in timed automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 198–212. Springer, Heidelberg (2013)
Olderog, E.-R., Dierks, H.: Real-time systems - formal specification and automatic verification. Cambridge University Press (2008)
Fitriani, K.: FraTTA: Framework for transformation of timed automata, Master Team Project, Albert-Ludwigs-Universität Freiburg (2013)
Dietsch, D., Feo-Arenis, S., et al.: Disambiguation of industrial standards through formalization and graphical languages. In: RE, pp. 265–270. IEEE (2011)
Gobriel, S., Khattab, S., Mossé, D., et al.: RideSharing: Fault tolerant aggregation in sensor networks using corrective actions. In: SECON, pp. 595–604. IEEE (2006)
Jensen, H., Larsen, K., Skou, A.: Modelling and analysis of a collision avoidance protocol using SPIN and Uppaal. In: 2nd SPIN Workshop (1996)
Steiner, W., Elmenreich, W.: Automatic recovery of the TTP/A sensor/actuator network. In: WISES, pp. 25–37, Vienna University of Technology (2003)
Kordy, P., Langerak, R., et al.: Re-verification of a lip synchronization protocol using robust reachability. In: FMA. EPTCS, vol. 20, pp. 49–62 (2009)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Herrera, C., Westphal, B., Podelski, A. (2014). Quasi-Equal Clock Reduction: More Networks, More Queries. In: Ábrahám, E., Havelund, K. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2014. Lecture Notes in Computer Science, vol 8413. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54862-8_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-54862-8_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54861-1
Online ISBN: 978-3-642-54862-8
eBook Packages: Computer ScienceComputer Science (R0)