Abstract
One of the major problems in applying automatic verification tools to industrial-size systems is the excessive amount of memory required during the state-space exploration of a model. In the setting of real-time, this problem of state-explosion requires extra attention as information must be kept not only on the discrete control structure but also on the values of continuous clock variables.
In this paper, we exploit Clock Difference Diagrams, CDD’s, a BDD-like data-structure for representing and effectively manipulating certain non- convex subsets of the Euclidean space, notably those encountered during verification of timed automata.
A version of the real-time verification tool Uppaal using CDD’s as a compact data-structure for storing explored symbolic states has been implemented. Our experimental results demonstrate significant spacesavings: for eight industrial examples, the savings are in average 42% with moderate increase in runtime.
We further report on how the symbolic state-space exploration itself may be carried out using CDD’s.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Asarain, Bozga, Kerbrat, Maler, Pnueli, Rasse. Data-Structures for the Verification of Timed Automata. In Proc. HART’97, LNCS 1201, pp. 346–360.
Alur, Dill. Automata for Modelling Real-Time Systems. In Proc. of ICALP’90, LNCS 443, 1990.
Felice Balarin. Approximate Reachability Analysis of Timed Automata. Proc. Real-Time Systems Symposium, Washington, DC, December 1996, pp. 52–61.
[BGK+96]_ Bengtsson, Griffioen, Kristoffersen, Larsen, Larsson, Pettersson, Yi. Verification of an audio protocol with bus collision using uppaal. CAV’96, LNCS 1102, 1996.
Bengtsson, Larsen, Larsson, Pettersson, Yi. Uppaal in 1995. In Proc. TACAS’96, LNCS 1055, pp. 431–434. Springer March 1996.
Bozga, Maler, Pnueli, Yovine. Some progress in the symbolic verification of timed automata. Proc. CAV’97, LNCS 1254,pp. 179–190, 1997.
Bosscher, Polak, Vaandrager. Verification of an Audio-control Protocol. In Proc. FTRTFT, LNCS 863, 1994.
Campos, Clarke. Real-time symbolic model checking for discrete time models. In C. Rattray T. Rus, Eds., AMAST Series in Computing: Theories and Experiences for Real-Time System Development, 1995.
Dill. Timing Assumptions and Verification of Finite-State Concurrent Systems. in: LNCS 407, Springer Berlin 1989, pp. 197–212.
D’Arginio, Katoen, Ruys, Tretmans. Bounded retransmission protocol must be on time! In Proc. TACAS’97, LNCS 1217, 1997.
Daws, Yovine. Two examples of verification of multirate timed automata with Kronos. In Proc. 16th IEEE Real-Time Systems Symposium, pp 66–75, Dec 95.
Henzinger, Nicollin, Sifakis, Yovine. Symbolic Model Checking for Real-Time Systems. Information and Computation, 111(2):193–244, 1994.
Henzinger, Ho, Wong-Toi. A Users Guide to HyTech. Technical report, Department of Computer Science, Cornell University, 1995.
Havelund, Larsen, Skou. Formal Verification of an Audio/Video Power Controller using the Real-Time Model Checker UPPAAL. Technical report made for Bang & Olufsen, 1998.
Havelund, Skou, Larsen, Lund. Formal Modelling and Analysis of an Audio/Video Protocol: An Industrial Case Study using UPPAAL. In In Proc. 18th IEEE Real-Time System Symposium, 1997.
Larsen, Pettersson, Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. In Proc. 16th IEEE Real-Time Systems Symposium, December 1995.
Larsen, Weise, Yi, Pearson. Clock Difference Diagrams. DoCS Technical Report No.98/99, Uppsala University, Sweden, presented at the Nordic Workshop on Programming Theory, Turku, Finland, November 1998.
Lönn, Pettersson, Yi. Formal Verification of a TDMA Protocol Start-Up Mechanism. In Proc. 1997 IEEE Pacific Rim International Symposium on Fault-Tolerant Systems, pp. 235–242, 1997.
Lindahl, Pettersson, Yi. Formal design and analysis of a gear controller. In Bernhard Steffen (Ed.), Proc. TACAS’98, LNCS 1384, pp. 281–297. Springer 1998.
Møller, Lichtenberg, Andersen, Hulgaard. Difference decision diagrams. Technical report IT-TR-1999-023, Technical University of Denmark, February 1999.
Møller, Lichtenberg, Andersen, Hulgaard. On the symbolic verification of timed systems. Technical report IT-TR-1999-024, Technical University of Denmark, February 1999.
Strehl, Thiele. Symbolic Model Checking of Process Networks Using Interval Diagram Techniques. ICCAD-98, San Jose, California, pp. 686–692, 1998.
Strehl. Using Interval Diagram Techniques for the Symbolic Verification of Timed Automata. Technical Report TIK-53, ETH Zürich, July 1998.
Wong-Toi, Dill. Verification of real-time systems by successive over and under approximation. CAV’95, July 1995.
Yi, Pettersson, Daniels. Automatic Verification of Real-Time Communicating Systems By Constraint-Solving. In Proc. 7th International Conference on Formal Description Techniques, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W. (1999). Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_30
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive