Abstract
Real-world real-time systems may involve many complex structures, which are difficult to verify. We experiment with the model-checking of an application-layer html-based web-camera which involves structures like event queues, high-layer communication channels, and time-outs. To contain the complexity, we implement our verification tool with a newly developed BDD-like data-structure, reduced CRD (Clock-Restriction Diagram), which has enhanced the verification performance through intensive data-sharing in a previous report. However, the representation of reduced CRD does not allow for quick test of zone containment. To this purpose, we thus have designed a new CRD-based representation, cascade CRD, which has given us enough performance enhancement to successfully verifying several implementations of the web-camera.
Keywords
Download to read the full chapter text
Chapter PDF
References
Asarin, Bozga, Kerbrat, Maler, Pnueli, Rasse. Data-Structures for the Verification of Timed Automata. Proceedings, HART’97, LNCS 1201.
R. Alur, C. Courcoubetis, D.L. Dill. Model Checking for Real-Time Systems, IEEE LICS, 1990.
F. Balarin. Approximate Reachability Analysis of Timed Automata. IEEE RTSS, 1996.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond, IEEE LICS, 1990.
M. Bozga, C. Daws. O. Maler. Kronos: A model-checking tool for real-time systems. 10th CAV, June/July 1998, LNCS 1427, Springer-Verlag.
J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, Wang Yi. UPPAAL-a Tool Suite for Automatic Verification of Real-Time Systems. Hybrid Control System Symposium, 1996, LNCS, Springer-Verlag.
G. Behrmann, K.G. Larsen, J. Pearson, C. Weise, Wang Yi. Efficient Timed Reachability Analysis Using Clock Difference Diagrams. CAV’99, July, Trento, Italy, LNCS 1633, Springer-Verlag.
R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation, IEEE Trans. Comput., C-35(8), 1986.
E. Clarke, O. Grumberg, M. Minea, D. Peled. State-Space Reduction using Partial-Ordering Techniques, STTT 2(3), 1999, pp.279–287.
D.L. Dill. Timing Assumptions and Verification of Finite-state Concurrent Systems. CAV’89, LNCS 407, Springer-Verlag.
C. Daws, A. Olivero, S. Tripakis, S. Yovine. The tool KRONOS. The 3rd Hybrid Systems, 1996, LNCS 1066, Springer-Verlag.
T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine. Symbolic Model Checking for Real-Time Systems, IEEE LICS 1992.
P.-A. Hsiung, F. Wang. User-Friendly Verification. Proceedings of 1999 FORTE/PSTV, October, 1999, Beijing. Formal Methods for Protocol Engineering and Distributed Systems, editors: J. Wu, S.T. Chanson, Q. Gao; Kluwer Academic Publishers.
K.G. Larsen, F. Larsson, P. Pettersson, Y. Wang. Efficient Verification of Real-Time Systems: Compact Data-Structure and State-Space Reduction. IEEE RTSS, 1998.
F. Wang. Efficient Data-Structure for Fully Symbolic Verification of Real-Time Software Systems. TACAS’2000, March, Berlin, Germany in LNCS, Springer-Verlag.
F. Wang. Region Encoding Diagram for Fully Symbolic Verification of Real-Time Systems. the 24th COMPSAC, Oct. 2000, Taipei, Taiwan, ROC, IEEE press.
F. Wang. Clock Restriction Diagram: Yet Another Data-Structure for Fully Symbolic Verification of Timed Automata, Technical Report TR-IIS-01-002, IIS, Academia Sinica, Taiwan, ROC.
F. Wang, P.-A. Hsiung. Automatic Verification on the Large. Proceedings of the 3rd IEEE HASE, November 1998.
S. Yovine. Kronos: A Verification Tool for Real-Time Systems. International Journal of Software Tools for Technology Transfer, Vol. 1, Nr. 1/2, October 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 IFIP International Federation for Information Processing
About this paper
Cite this paper
Wang, F. (2001). Symbolic Verification of Complex Real-time Systems with Clock-restriction Diagram. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds) Formal Techniques for Networked and Distributed Systems. FORTE 2001. IFIP International Federation for Information Processing, vol 69. Springer, Boston, MA. https://doi.org/10.1007/0-306-47003-9_15
Download citation
DOI: https://doi.org/10.1007/0-306-47003-9_15
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-7923-7470-1
Online ISBN: 978-0-306-47003-5
eBook Packages: Springer Book Archive