Numerical Coverage Estimation for the Symbolic Simulation of Real-Time Systems

  • Farn Wang
  • Geng-Dian Hwang
  • Fang Yu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2767)


Three numerical coverage metrics for the symbolic simulation of dense-time systems and their estimation methods are presented. Special techniques to derive numerical estimations of dense-time state-spaces have also been developed. Properties of the metrics are also discussed with respect to four criteria. Implementation and experiments are then reported.


coverage verification symbolic simulation real-time 


  1. 1.
    Alur, R., Courcoubetis, C., Dill, D.L.: Model Checking for Real-Time Systems. IEEE LICS (1990) Google Scholar
  2. 2.
    Alur, R., Dill, D.L.: Automata for modelling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  3. 3.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. IEEE LICS (1990)Google Scholar
  4. 4.
    Beizer, B.: Software Testing Techniques, 2nd edn. Van Nostrand Rheinhold, New York (1990)zbMATHGoogle Scholar
  5. 5.
    Bening, L., Foster, H.: Principles of Verifiable RTL Design, a Functional Coding Style Supporting Verification Processes in Verilog, 2nd edn. Kluwer Academic Publishers, Dordrecht (2001)zbMATHGoogle Scholar
  6. 6.
    Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Bryant, R.E.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Trans. Comput. C-35(8) (1986)Google Scholar
  8. 8.
    Cheng, K.-T., Krishnakumar, A.S.: Automatic Functional Test Generation Using the Extended Finite State Machine Model. In: Proceedings of the 30th Design Automation Conference, pp. 86–91 (June 1993)Google Scholar
  9. 9.
    Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage Metrics for Temporal Logic Model Checking. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 528–552. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  10. 10.
    Devadas, S., Ghosh, A., Keutzer, K.: An Obervability-Based Code Coverage Metric for Functional Simulation. IEEE ICCAD 1996 (1996) Google Scholar
  11. 11.
    Dill, D.L.: Timing Assumptions and Verification of Finite-state Concurrent Systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  12. 12.
    Dill, D.L.: What’s Between Simulation and Formal Verification? In: Proceedings of DAC1998 (1998) Google Scholar
  13. 13.
    Fallah, F., Devadas, S., Keutzer, K.: OCCOM: Efficient Computation of Observability-Based Code Coverage Metrics for Functional Verification. In: Design Automation Conference, pp. 152–157 (1998)Google Scholar
  14. 14.
    Geist, D., Farkas, M., Landver, A., Lichtenstein, Y., Ur, S., Wolsfthal, Y.: Coverage-Directed Test Generation Using Symbolic Techniques. In: Proceedings of the Int’l Conference on Formal Methods in CAD (November 1996)Google Scholar
  15. 15.
    Haartsen, J.: Bluetooth Specification, version 1.0,
  16. 16.
    Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Model Checking for Real-Time Systems. In: IEEE LICS 1992 (1992) Google Scholar
  17. 17.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  18. 18.
    Hoskote, Y., Moundanos, D., Abraham, J.: Automatic Extraction of the Control Flow Machine and Application to Evaluating Coverage of Verification Vectors. In: Proceedings of ICCD, pp. 532–537 (October 1995)Google Scholar
  19. 19.
    Hoskote, Y., Moundanos, D., Abraham, J.A.: Automatic Extraction of the control flow machine and application to evaluating coverage of verification vectors. In: Proceedings of the Int’l Conference on Computer Design, pp. 532–537 (October 1995)Google Scholar
  20. 20.
    Hoskote, Y., Kam, T., Ho, P.-H., Zhao, X.: Coverage estimation for symbolic model checking. In: Proceedings of DAC1999, pp. 300–305 (1999)Google Scholar
  21. 21.
    Larsen, K.G., Pettersson, P., Yi, W.: Model-Checking for Real-Time Systems. In: Proceedings of the 10th International Conference on Fundamentals of Computation Theory, Dresden, Germany. LNCS, vol. 965, pp. 62–88. Horst Reichel (1995)Google Scholar
  22. 22.
    Mike, B., Daniel, G., Alan, H., Yaron, W., Gerard, M., Ralph, S.: A Study in Coverage-Driven Test Generation. In: Proceedings of DAC 1999, pp. 970–975 (1999)Google Scholar
  23. 23.
    Pettersson, P., Larsen, K.G.: UPPAAL2k. In: Bulletin of the European Association for Theoretical Computer Science, vol. 70, pp. 40–44 (2000)Google Scholar
  24. 24.
    Rashinkar, P., Paterson, P., Singh, L.: System-on-a-chip Verification, Methodology and Techniques. Kluwer Academic Publishers, Dordrecht (2001)zbMATHGoogle Scholar
  25. 25.
    Seger, C.-J.H., Bryant, R.E.: Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories. Formal Methods in System Designs 6(2), 147–189 (1995)CrossRefGoogle Scholar
  26. 26.
    Wang, F.: Efficient Data-Structure for Fully Symbolic Verification of Real-Time Software Systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, p. 157. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  27. 27.
    Wang, F.: Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram. In: Proceedings of FORTE, Cheju Island, Korea (2001) (to appear)Google Scholar
  28. 28.
    Wang, F.: Efficient Verification of Timed Automata with BDD-like Data-Structures. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 189–205. Springer, Heidelberg (2002) (to appear)CrossRefGoogle Scholar
  29. 29.
    Wang, F., Hwang, G.-D., Yu, F.: Symbolic Simulation of Real-Time Concurrent Systems. In: Chen, J., Hong, S. (eds.) RTCSA 2003. LNCS, vol. 2968, pp. 595–617. Springer, Heidelberg (2004) (to appear)CrossRefGoogle Scholar
  30. 30.
    Yovine, S.: Kronos: A Verification Tool for Real-Time Systems. International Journal of Software Tools for Technology Transfer 1(1/2) (October 1997)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Farn Wang
    • 1
  • Geng-Dian Hwang
    • 2
  • Fang Yu
    • 2
  1. 1.Dept. of Electrical EngineeringNational Taiwan UniversityTaipeiTaiwan, Republic of China
  2. 2.Institute of Information ScienceAcademia SinicaTaipeiTaiwan, Republic of China

Personalised recommendations