Advertisement

CAVEAT: technique and tool for computer aided verification and transformation

  • E. Pascal Gribomont
  • Didier Rossetto
Session 3: Invited Talk
Part of the Lecture Notes in Computer Science book series (LNCS, volume 939)

Abstract

We describe caveat, a technique and a tool (under development) for the stepwise design and verification of nearly finite-state concurrent systems (NFCS). A concurrent system is nearly finite-state when most of its variables have a finite range (Booleans, bounded integers). The heart of caveat is a tool for verifying invariants, i.e., inductive safety properties. The underlying method is classical: formula I is an invariant for system S if and only if some formula ΦI=def {I}S{I} is valid. If S is an NFCS, the formula ΦI contains only a small set of non-boolean variables. caveat uses the connection method to extract from ΦI a (small) set Ψ of paths (some kind of assertions) about the non-boolean variables; ΦI is valid if and only if all paths contain connections, i.e., are inconsistent. For typical NFCS given with a correct invariant, the formula ΦI is rather large (more than 100 lines) but Ψ is quite small (a dozen one-line formulas). The second part of caveat (not implemented yet) supports an incremental development method that is fairly systematic, but has proved to be flexible enough in practice.

Keywords

Model Check Temporal Logic Mutual Exclusion Safety Property Concurrent System 
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.
    K.R. Apt and D.C. Kozen, Limits for Automatic Program Verification, Inform. Process. Letters 22 (1986) 307–309.Google Scholar
  2. 2.
    R.J. Back, A Method for Refining Atomicity in Parallel Algorithms, PARLE'89, Lect. Notes in Comput. Sci. 366 (1989) 199–216.Google Scholar
  3. 3.
    R.J. Back and R. Kurki-Suonio, Distributed co-operation with action systems, ACM Trans. Programming Languages Syst. 10 (1988) 513–554.Google Scholar
  4. 4.
    S. Bensalem et al., Property Preserving Abstractions for the Verification of Concurrent Systems, to appear in Formal Methods in System Design (1994).Google Scholar
  5. 5.
    W. Bibel, Deduction — Automated Logic, Academic Press, 1993.Google Scholar
  6. 6.
    R.E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Trans. on Computers C-35 (1986) 677–691.Google Scholar
  7. 7.
    J.R. Burch et al., Symbolic Model Checking: 1020 States and Beyond, Proc. 5th. Symp. on Logic in Computer Science (1990) 428–439.Google Scholar
  8. 8.
    E. Clarke, E. Emerson and A. Sistla, Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications, ACM Trans. Programming Languages Syst. 8 (1986) 244–263.Google Scholar
  9. 9.
    E.W. Dijkstra and al., On-the-Fly Garbage Collection: An Exercise in Cooperation, Comm. ACM 21 (1978) 966–975.CrossRefGoogle Scholar
  10. 10.
    T. Elrad and N. Francez, Decomposition of Distributed Programs into Communication-closed Layers, Sci. Comput. Programming 2 (1982) 155–173.Google Scholar
  11. 11.
    D.M. Goldschlag, Mechanically Verifying Concurrent Programs with the Boyer-Moore Prover, IEEE Trans. on Software Eng. 16 (1990) 1005–1023.Google Scholar
  12. 12.
    S. Graf, Verification of a distributed Cache memory by using abstractions, Lect. Notes in Comput. Sci. 818 (1994) 207–219.Google Scholar
  13. 13.
    E.P. Gribomont, Synthesis of parallel programs invariants, TAPSOFT'85, Lect. Notes in Comput. Sci. 186 (1985) 325–338.Google Scholar
  14. 14.
    E.P. Gribomont, Stepwise refinement and concurrency: the finite-state case, Sci. Comput. Programming 14 (1990) 185–228.Google Scholar
  15. 15.
    E.P. Gribomont, Design, verification and documentation of concurrent systems, in Proc. 4th. Refinement workshop, J.M. Morris and R.C. Shaw (Eds), pp. 360–377, Springer-Verlag, 1991.Google Scholar
  16. 16.
    E.P. Gribomont, Concurrency without toil: a systematic method for parallel program design”. Sci. Comput. Programming 21 (1993) 1–56.MathSciNetGoogle Scholar
  17. 17.
    N. Halbwachs and F. Maraninchi, On the symbolic analysis of combinational loops in circuits and synchronous programs, REACT Report, 1994.Google Scholar
  18. 18.
    B. Jonsson, Compositional Specification and Verification of Distributed System, ACM Trans. Programming Languages Syst. 16 (1994) 259–303.Google Scholar
  19. 19.
    R.P. Kurshan and L. Lamport, Verification of a Multiplier: 64 Bits and Beyond, CAV'93, Lect. Notes in Comput. Sci. 697 (1993) 166–179.Google Scholar
  20. 20.
    R.P. Kurshan and M. McMillan, A structural induction theorem for processes, Proc. 8th ACM Symp. on Principles of Distributed Computing, Edmonton (1989).Google Scholar
  21. 21.
    L. Lamport, An Assertional Correctness Proof of a Distributed Algorithm, Sci. Comput. Programming 2 (1983) 175–206.Google Scholar
  22. 22.
    L. Lamport and F.B. Schneider, Pretending Atomicity, DEC SRC Rep. 44, May 1989.Google Scholar
  23. 23.
    R. Letz, J. Schumann, S. Bayerl and W. Bibel, SETHEO: A High-Performance Theorem Prover, Jl. of Automated Reasoning 8 (1992) 183–212.Google Scholar
  24. 24.
    N.A. Lynch and M.R. Tuttle, Hierarchical Correctness Proofs for Distributed Algorithms, Proc. 6th ACM Symp. on Principles of Distributed Computing, New-York (1987) 137–151.Google Scholar
  25. 25.
    Z. Manna et al., Step: the Stanford Temporal Prover (Draft), June 1994.Google Scholar
  26. 26.
    J.S. Moore, Introduction to the OBDD algorithm for the ATP Community, Jl. of Automated Reasoning 12 (1994) 33–45.Google Scholar
  27. 27.
    G. Ricart and A.K. Agrawala, An optimal algorithm for mutual exclusion, Comm. ACM 24 (1981) 9–17 (corrigendum: Comm. ACM 24 (1981) 578).Google Scholar
  28. 28.
    F. Stomp and W.P. de Roever, A principle for sequential phased reasoning about distributed systems, Formal Aspects of Computing 6 (1994) 716–737.Google Scholar
  29. 29.
    M.Y. Vardi, P. Wolper, An Automata-Theoretic Approach To Automatic Program Verification, Proc. Symp. on Logic in Comput. Sci., Cambridge (1986) 322–331.Google Scholar
  30. 30.
    P. Wolper and V. Lovinfosse, Verifying Properties of large Sets of Processes with Network Invariants, CAV'89, Lect. Notes in Comput. Sci. 407 (1990) 68–80.Google Scholar
  31. 31.
    L. Wallen, Automated Deduction in Nonclassical Logics, MIT Press, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • E. Pascal Gribomont
    • 1
  • Didier Rossetto
    • 1
  1. 1.Institut MontefioreUniversité de LiègeLiègeBelgium

Personalised recommendations