Abstract
This paper addresses Zeno runs, i.e., transition sequences that can execute arbitrarily fast, in the context of model checking with the UPPAAL tool. Zeno runs conflict with real-world experience where execution always takes time and they may introduce timelocks into the models. We enhance previous work on static detection of Zeno runs by extending synchronization exploitation using a synchronization matrix that not only ensures valid synchronization partners exist but also that their number is correct. Additionally, we introduce two data-variable heuristics into the analysis as in most models data-variable constraints prevent certain Zeno runs. The analysis is implemented in a tool called ZenoTool and empirically evaluated using 13 benchmarks. The evaluation shows that our analysis is more accurate in 3 cases and never less accurate than the analysis results of previous work and that performance and memory overhead are at the same time very low.
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.
Similar content being viewed by others
References
Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Transactions on Programming Languages and Systems 16(5), 1543–1571 (1994)
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138, 3–34 (1995)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Bornot, S., Sifakis, J.: Relating time progress and deadlines in hybrid systems. In: Proc. of the Int. Work. on Hybrid and Real-Time Systems, pp. 286–300 (1997)
Bornot, S., Sifakis, J.: On the Composition of Hybrid Systems. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol. 1386, pp. 49–63. Springer, Heidelberg (1998)
Bornot, S., Sifakis, J., Tripakis, S.: Modeling urgency in timed systems. In: Int. Symp.: Compositionality - The Significant Difference, pp. 103–129 (1997)
Bowman, H.: Time and action lock freedom properties of timed automata. In: Formal Techniques for Networked and Distributed Systems, pp. 119–134 (2001)
Bowman, H., Faconti, G., Katoen, J.-P., Latella, D., Massink, M.: Automatic verification of a lip-synchronisation protocol using UPPAAL. Formal Aspects of Computing 10, 550–575 (1998)
Bowman, H., Gómez, R.: How to stop time stopping. Formal Aspects of Computing 18, 459–493 (2006)
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)
Gebremichael, B., Vaandrager, F.: Specifying urgency in timed I/O automata. In: Proc. of the 3rd IEEE Int. Conf. on Software Engineering and Formal Methods, pp. 64–73 (2005)
Gebremichael, B., Vaandrager, F., Zhang, M.: Analysis of the zeroconf protocol using UPPAAL. In: Proc. of the 6th ACM & IEEE Int. Conf. on Embedded Software, pp. 242–251 (2006)
Gómez, R., Bowman, H.: Discrete Timed Automata and MONA: Description, Specification and Verification of a Multimedia Stream. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 177–192. Springer, Heidelberg (2003)
Gómez, R., Bowman, H.: Efficient Detection of Zeno Runs in Timed Automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 195–210. Springer, Heidelberg (2007)
Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL. In: Proc. of the 18th IEEE Real-Time Systems Symp., pp. 2–13 (1997)
Henzinger, T.A.: The theory of hybrid automata. In: LICS: Logic in Computer Science. pp. 278–292. IEEE Computer Society Press (1996)
Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Efficient Emptiness Check for Timed Büchi Automata. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 148–161. Springer, Heidelberg (2010)
Kaynar, D.K., Lynch, N., Segala, R., Vaandrager, F.: The theory of timed I/O automata, 2nd ed. Synthesis Lectures on Dist. Comp. Theory 1(1), 1–137 (2010)
Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. 5(1), 1–11 (1987)
Lindahl, M., Pettersson, P., Yi, W.: Formal Design and Analysis of a Gear Controller. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 281–297. Springer, Heidelberg (1998)
Lönn, H., Pettersson, P.: Formal verification of a TDMA protocol start-up mechanism. In: Proc. of the 1997 Pacific Rim Int. Symp. on Fault-Tolerant Systems, pp. 235–242 (1997)
Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. Ph.D. thesis, Cambridge, MA, USA (1974)
Rinast, J.: ZenoTool, A Zeno Run detection tool for UPPAAL, http://www.sts.tu-harburg.de/research/zenotool.html
Szwarcfiter, J.L., Lauer, P.E.: A search strategy for the elementary cycles of a directed graph. BIT Numerical Mathematics 16, 192–204 (1976)
Tarjan, R.E.: Enumeration of the elementary circuits of a directed graph. Tech. rep., Department of Computer Science, Cornell University, Ithaca, NY, USA (1972)
Tiernan, J.C.: An efficient search algorithm to find the elementary circuits of a graph. Commun. ACM 13, 722–726 (1970)
Tripakis, S.: Verifying Progress in Timed Systems. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 299–314. Springer, Heidelberg (1999)
Tripakis, S., Yovine, S., Bouajjani, A.: Checking Timed Büchi Automata Emptiness Efficiently. Formal Methods in System Design 26, 267–292 (2005)
Vaandrager, F., de Groot, A.: Analysis of a biphase mark protocol with UPPAAL and PVS. Formal Aspects of Computing 18, 433–458 (2006)
Yovine, S.: Kronos: a verification tool for real-time systems. International Journal on Software Tools for Technology Transfer (STTT) 1, 123–133 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rinast, J., Schupp, S. (2012). Static Detection of Zeno Runs in UPPAAL Networks Based on Synchronization Matrices and Two Data-Variable Heuristics. In: Jurdziński, M., Ničković, D. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2012. Lecture Notes in Computer Science, vol 7595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33365-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-33365-1_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33364-4
Online ISBN: 978-3-642-33365-1
eBook Packages: Computer ScienceComputer Science (R0)