Advertisement

Static Detection of Zeno Runs in UPPAAL Networks Based on Synchronization Matrices and Two Data-Variable Heuristics

  • Jonas Rinast
  • Sibylle Schupp
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7595)

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.

Keywords

Zeno Runs Timed Automata UPPAAL 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Transactions on Programming Languages and Systems 16(5), 1543–1571 (1994)CrossRefGoogle Scholar
  2. 2.
    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)MathSciNetzbMATHCrossRefGoogle Scholar
  3. 3.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    Bornot, S., Sifakis, J., Tripakis, S.: Modeling urgency in timed systems. In: Int. Symp.: Compositionality - The Significant Difference, pp. 103–129 (1997)Google Scholar
  7. 7.
    Bowman, H.: Time and action lock freedom properties of timed automata. In: Formal Techniques for Networked and Distributed Systems, pp. 119–134 (2001)Google Scholar
  8. 8.
    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)zbMATHCrossRefGoogle Scholar
  9. 9.
    Bowman, H., Gómez, R.: How to stop time stopping. Formal Aspects of Computing 18, 459–493 (2006)zbMATHCrossRefGoogle Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    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)Google Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    Henzinger, T.A.: The theory of hybrid automata. In: LICS: Logic in Computer Science. pp. 278–292. IEEE Computer Society Press (1996)Google Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    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)CrossRefGoogle Scholar
  19. 19.
    Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. 5(1), 1–11 (1987)CrossRefGoogle Scholar
  20. 20.
    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)CrossRefGoogle Scholar
  21. 21.
    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)Google Scholar
  22. 22.
    Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. Ph.D. thesis, Cambridge, MA, USA (1974)Google Scholar
  23. 23.
    Rinast, J.: ZenoTool, A Zeno Run detection tool for UPPAAL, http://www.sts.tu-harburg.de/research/zenotool.html
  24. 24.
    Szwarcfiter, J.L., Lauer, P.E.: A search strategy for the elementary cycles of a directed graph. BIT Numerical Mathematics 16, 192–204 (1976)MathSciNetzbMATHCrossRefGoogle Scholar
  25. 25.
    Tarjan, R.E.: Enumeration of the elementary circuits of a directed graph. Tech. rep., Department of Computer Science, Cornell University, Ithaca, NY, USA (1972)Google Scholar
  26. 26.
    Tiernan, J.C.: An efficient search algorithm to find the elementary circuits of a graph. Commun. ACM 13, 722–726 (1970)MathSciNetzbMATHCrossRefGoogle Scholar
  27. 27.
    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)CrossRefGoogle Scholar
  28. 28.
    Tripakis, S., Yovine, S., Bouajjani, A.: Checking Timed Büchi Automata Emptiness Efficiently. Formal Methods in System Design 26, 267–292 (2005)zbMATHCrossRefGoogle Scholar
  29. 29.
    Vaandrager, F., de Groot, A.: Analysis of a biphase mark protocol with UPPAAL and PVS. Formal Aspects of Computing 18, 433–458 (2006)zbMATHCrossRefGoogle Scholar
  30. 30.
    Yovine, S.: Kronos: a verification tool for real-time systems. International Journal on Software Tools for Technology Transfer (STTT) 1, 123–133 (1997)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Jonas Rinast
    • 1
  • Sibylle Schupp
    • 1
  1. 1.Institute for Software SystemsHamburg University of TechnologyHamburgGermany

Personalised recommendations