# CAVEAT: technique and tool for computer aided verification and transformation

## 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## References

- 1.K.R. Apt and D.C. Kozen, Limits for Automatic Program Verification,
*Inform. Process. Letters***22**(1986) 307–309.Google Scholar - 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.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.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.W. Bibel,
*Deduction — Automated Logic*, Academic Press, 1993.Google Scholar - 6.R.E. Bryant, Graph-based algorithms for Boolean function manipulation,
*IEEE Trans. on Computers***C-35**(1986) 677–691.Google Scholar - 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.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.E.W. Dijkstra and al., On-the-Fly Garbage Collection: An Exercise in Cooperation,
*Comm. ACM***21**(1978) 966–975.CrossRefGoogle Scholar - 10.T. Elrad and N. Francez, Decomposition of Distributed Programs into Communication-closed Layers,
*Sci. Comput. Programming***2**(1982) 155–173.Google Scholar - 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.S. Graf, Verification of a distributed Cache memory by using abstractions,
*Lect. Notes in Comput. Sci.***818**(1994) 207–219.Google Scholar - 13.E.P. Gribomont, Synthesis of parallel programs invariants, TAPSOFT'85,
*Lect. Notes in Comput. Sci.***186**(1985) 325–338.Google Scholar - 14.E.P. Gribomont, Stepwise refinement and concurrency: the finite-state case,
*Sci. Comput. Programming***14**(1990) 185–228.Google Scholar - 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.E.P. Gribomont, Concurrency without toil: a systematic method for parallel program design”.
*Sci. Comput. Programming***21**(1993) 1–56.MathSciNetGoogle Scholar - 17.N. Halbwachs and F. Maraninchi, On the symbolic analysis of combinational loops in circuits and synchronous programs, REACT Report, 1994.Google Scholar
- 18.B. Jonsson, Compositional Specification and Verification of Distributed System,
*ACM Trans. Programming Languages Syst.***16**(1994) 259–303.Google Scholar - 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.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.L. Lamport, An Assertional Correctness Proof of a Distributed Algorithm,
*Sci. Comput. Programming***2**(1983) 175–206.Google Scholar - 22.L. Lamport and F.B. Schneider, Pretending Atomicity, DEC SRC Rep. 44, May 1989.Google Scholar
- 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.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.Z. Manna et al., Step: the Stanford Temporal Prover (Draft), June 1994.Google Scholar
- 26.J.S. Moore, Introduction to the OBDD algorithm for the ATP Community,
*Jl. of Automated Reasoning***12**(1994) 33–45.Google Scholar - 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.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.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.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.L. Wallen,
*Automated Deduction in Nonclassical Logics*, MIT Press, 1990.Google Scholar