Advertisement

Verification of real-time systems by successive over and under approximation

  • David L. Dill
  • Howard Wong-Toi
Session 12: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

Abstract

Automata-theoretic techniques provide a powerful means of verifying finite-bounded systems. However they suffer from state explosion. One approach to this problem is to analyze an abstracted system description. In safety verification, different abstractions can yield true lower or upper approximations of the set of reachable states. Previously, we presented an algorithm [24] which uses simple heuristics to automatically generate finer abstractions until the approximations correctly answer the verification problem.

In this paper, we extend the algorithm to include approximations over the system's transition structure as well as its state space. In terms of real-time system verification, this enables us to efficiently verify properties of the full class of timed safety automata augmented with urgency semantics. We describe a case study involving some bounded liveness properties of the MAC sublayer of the Ethernet protocol, based on a description by Weinberg and Zuck. This example is substantially more difficult than those verified by previously published real-time verification techniques.

Keywords

Control Location Symbolic Representation Time Zone Reachable State Frame Transmitter 
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

  1. 1.
    R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi. Minimization of timed transition systems (extended abstract). In Proc. of 3rd CONCUR, LNCS 630, Springer-Verlag, 1992.Google Scholar
  2. 2.
    R. Alur and D.L. Dill. Automata for modeling real-time systems. In Proc. of 17th ICALP, LNCS 443, Springer-Verlag, 1990.Google Scholar
  3. 3.
    R. Alur, A. Itai, R. Kurshan, and M. Yannakakis. Timing verification by successive approximation. In Proc. of 4th CAV, LNCS 663, Springer-Verlag, 1993.Google Scholar
  4. 4.
    F. Balarin and A.L. Sangiovanni-Vincentelli. A verification strategy for timing constrained systems. In Proc. of 4th CAV, LNCS 663, Springer-Verlag, 1993.Google Scholar
  5. 5.
    F. Balarin and A.L. Sangiovanni-Vincentelli. Iterative algorithms for formal verification of embedded real-time systems. In Proc. of ICCAD, 1994.Google Scholar
  6. 6.
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.Google Scholar
  7. 7.
    J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. of 5th LICS, 1990.Google Scholar
  8. 8.
    P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of 4th POPL, 1977.Google Scholar
  9. 9.
    P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2–3):103–179, July 1992.CrossRefGoogle Scholar
  10. 10.
    D. Dams, R. Gerth, G. Döhmen, R. Herrmann, P. Kelb, and H. Pargmann. Model checking using adaptive state and data abstraction. In Proc. of 6th CAV, LNCS 818, Springer-Verlag, 1994.Google Scholar
  11. 11.
    D. Dams, R. Gerth, and O. Grumberg. Generation of reduced models for checking fragments of CTL. In Proc. of 5th CAV, LNCS 697, Springer-Verlag, 1993.Google Scholar
  12. 12.
    D.L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems, International Workshop. LNCS 407, Springer-Verlag, 1989.Google Scholar
  13. 13.
    N. Halbwachs. Delay analysis in synchronous programs. In Proc. of 5th CAV, LNCS 697, Springer-Verlag, 1993.Google Scholar
  14. 14.
    T.A. Henzinger and P.-H. Ho. Model checking strategies for hybrid systems. In Proc. of the International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, 1994.Google Scholar
  15. 15.
    T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proc. of 7th LICS, 1992.Google Scholar
  16. 16.
    I. Kang and I. Lee. An efficient generation of the timed reachability graph for the analysis of real-time systems. Technical Report MS-CIS-94-36, University of Pennsylvania, 1994.Google Scholar
  17. 17.
    K.L. McMillan and P.H. Ho. Automatic timing analysis of timed circuits. Unpublished manuscript. 1994.Google Scholar
  18. 18.
    V.G. Naik and A.P. Sistla. Modeling and verification of a real life protocol using symbolic model checking. In Proc. of 6th CAV, LNCS 818, Springer-Verlag, 1994.Google Scholar
  19. 19.
    X. Nicollin, J. Sifakis, and S. Yovine. Compiling real-time specifications into extended automata. IEEE Transactions on Software Engineering, SE-18(9):794–804, 1992.Google Scholar
  20. 20.
    J.S. Ostroff. Verification of safety critical systems using TTM/RTTL. In Proc. of 1991 REX Workshop in “Real-Time: Theory in Practice”, LNCS 600, Springer-Verlag, 1992.Google Scholar
  21. 21.
    T.G. Rokicki and C.J. Myers. Automatic verification of timed circuits. In Proc. of 6th CAV, LNCS 818, Springer-Verlag, 1994.Google Scholar
  22. 22.
    H.B. Weinberg and L.D. Zuck. Timed ethernet: Real-time formal specification of ethernet. In Proc. of 3rd CONCUR, LNCS 630, Springer-Verlag, 1992.Google Scholar
  23. 23.
    H. Wong-Toi. Symbolic Approximations for Verifying Real-Time Systems. PhD thesis, Dept. of Computer Science, Stanford University, CA, December 1994.Google Scholar
  24. 24.
    H. Wong-Toi and D.L. Dill. Approximations for verifying timing properties. In Theories and Experiences for Real-Time System Development, chapter 7. World Scientific, 1995.Google Scholar
  25. 25.
    M. Yannakakis and D. Lee. An efficient algorithm for minimizing real-time transition systems. In Proc. of 5th CAV, LNCS 697, Springer-Verlag, 1993.Google Scholar
  26. 26.
    T. Yoneda, Y. Tohma, and Y. Kondo. Acceleration of timing verification method based on time petri nets. Systems and Computers in Japan, 22(12):37–52, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • David L. Dill
    • 1
  • Howard Wong-Toi
    • 2
  1. 1.Department of Computer ScienceStanford University
  2. 2.Department of Computer ScienceCornell University

Personalised recommendations