Advertisement

What if model checking must be truly symbolic

  • Hardi Hungar
  • Orna Grumberg
  • Werner Damm
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)

Abstract

There are many methodologies whose main concern is reducing the complexity of a verification problem to be ultimately able to apply model checking. Here we propose to use a model-checking like procedure which operates on a small, truly symbolic description of the model. We do so by exploiting systematically the separation between the (small) control part and the (large) data part of systems which often occurs in practice. By expanding the control part, we get an intermediate description of the system which already allows our symbolic model checking procedure to produce meaningful results but which is still small enough to allow model checking to be performed.

Keywords

Model Check Recurrence Node Control Part Label Transition System Verification Condition 
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.
    Apt, K.R. Ten years of Hoare's logic: A survey — part I, TOPLAS 3 (1981), 431–483.Google Scholar
  2. 2.
    Apt, K.R. and Olderog, E.-R. Verification of sequential and concurrent programs, Springer, New York (1991).Google Scholar
  3. 3.
    Bradfield, J.C. Verifying temporal properties of systems, BirkhÄuser, Boston (1992).Google Scholar
  4. 4.
    Bradfield, J.C. and Stirling, C.P. Verifying temporal properties of processes, CONCUR '90, LNCS 458 (1990), 115–125.Google Scholar
  5. 5.
    Brown,M.C., Clarke, E.M. and Grumberg, O. Characterizing finite Kripke structures in propositional temporal logic, TCS 59 (1988), 115–131.Google Scholar
  6. 6.
    Burch, J.R., Clarke, E.M., McMillan, K.L. and Dill D.L. Sequential circuit verification using symbolic model checking DAC '90, 46–51.Google Scholar
  7. 7.
    Clarke, E.M., Emerson, E.A. and Sistla, A.P. Automatic verification of finite state concurrent systems using temporal logics, POPL '83, 117–126.Google Scholar
  8. 8.
    Clarke, E.M., Grumberg, O. and Long, D.E. Model checking and abstraction, POPL '92, 343–354.Google Scholar
  9. 9.
    Damm, W., Döhmen, G., Helbig, J., Herrmann, R., Josko, B., Kelb, P., Korf, F. and Schlör, R. Correct system level design with VHDL, Tech. Rep., Oldenburg (1994), 54p.Google Scholar
  10. 10.
    Damm, W., Josko, B. and Schlör, R. Specification and verification of VHDL-based system-level hardware designs, in Börger (ed.) Specification and Validation Methods, Oxford Univ. Press, 331–410 (to appear).Google Scholar
  11. 11.
    Dingel, J. and Filkorn, T. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving, CAV '95, to appear.Google Scholar
  12. 12.
    Emerson, E.A. Temporal and modal logic, in: Handbook of Theor. Comp. Sc., B, North Holland (1990), 997–1072.Google Scholar
  13. 13.
    Floyd, R.W. Assigning meanings to programs, Proc. AMS Symp. Applied Math. 19 (1967), 19–31.Google Scholar
  14. 14.
    Graf, S. Verification of a distributed cache memory by using abstractions, CAV '94, LNCS 818 (1994), 207–219.Google Scholar
  15. 15.
    Grumberg, O. and Long, D.E. Model checking and modular verification, TOPLAS 16 (1994), 843–871.Google Scholar
  16. 16.
    Herrmann, R. and Pargmann, H. Compiling VHDL data types into BDDs, EURO-VHDL '94, 578–583.Google Scholar
  17. 17.
    Hojati, R. and Brayton, R.K. Automatic datapath abstraction in hardware systems, CAV '95, to appear.Google Scholar
  18. 18.
    Josko, B. Verifying the correctness of AADL modules using model checking, in: Stepwise refinement of distributed systems: models, formalisms, correctness, LNCS 430 (1990), 386–400.Google Scholar
  19. 19.
    Manna, Z. Beyong model checking, CAV '94, LNCS 818 (1994), 220–221.Google Scholar
  20. 20.
    Manna, Z. and Pnueli, A. The temporal logics of reactive and concurrent systems. Specification. Springer, New York 1992.Google Scholar
  21. 21.
    Schlör, R. and Damm, W. Specification and verification of system-level hardware designs using timing diagrams, EDAC '93, 518–524.Google Scholar
  22. 22.
    Stirling, C. and Walker, D. Local model checking in the modal mu-calculus, TAPSOFT '89, LNCS 351, 369–383.Google Scholar
  23. 23.
    Wolper, P. Expressing interesting properties of programs in propositional temporal logic, POPL '86, 184–193.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Hardi Hungar
    • 1
  • Orna Grumberg
    • 2
  • Werner Damm
    • 3
  1. 1.OFFISOldenburg
  2. 2.The TechnionHaifa
  3. 3.University OldenburgGermany

Personalised recommendations