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.
Chapter PDF
Similar content being viewed by others
Keywords
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
K.R. Apt and D.C. Kozen, Limits for Automatic Program Verification, Inform. Process. Letters 22 (1986) 307–309.
R.J. Back, A Method for Refining Atomicity in Parallel Algorithms, PARLE'89, Lect. Notes in Comput. Sci. 366 (1989) 199–216.
R.J. Back and R. Kurki-Suonio, Distributed co-operation with action systems, ACM Trans. Programming Languages Syst. 10 (1988) 513–554.
S. Bensalem et al., Property Preserving Abstractions for the Verification of Concurrent Systems, to appear in Formal Methods in System Design (1994).
W. Bibel, Deduction — Automated Logic, Academic Press, 1993.
R.E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Trans. on Computers C-35 (1986) 677–691.
J.R. Burch et al., Symbolic Model Checking: 1020 States and Beyond, Proc. 5th. Symp. on Logic in Computer Science (1990) 428–439.
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.
E.W. Dijkstra and al., On-the-Fly Garbage Collection: An Exercise in Cooperation, Comm. ACM 21 (1978) 966–975.
T. Elrad and N. Francez, Decomposition of Distributed Programs into Communication-closed Layers, Sci. Comput. Programming 2 (1982) 155–173.
D.M. Goldschlag, Mechanically Verifying Concurrent Programs with the Boyer-Moore Prover, IEEE Trans. on Software Eng. 16 (1990) 1005–1023.
S. Graf, Verification of a distributed Cache memory by using abstractions, Lect. Notes in Comput. Sci. 818 (1994) 207–219.
E.P. Gribomont, Synthesis of parallel programs invariants, TAPSOFT'85, Lect. Notes in Comput. Sci. 186 (1985) 325–338.
E.P. Gribomont, Stepwise refinement and concurrency: the finite-state case, Sci. Comput. Programming 14 (1990) 185–228.
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.
E.P. Gribomont, Concurrency without toil: a systematic method for parallel program design”. Sci. Comput. Programming 21 (1993) 1–56.
N. Halbwachs and F. Maraninchi, On the symbolic analysis of combinational loops in circuits and synchronous programs, REACT Report, 1994.
B. Jonsson, Compositional Specification and Verification of Distributed System, ACM Trans. Programming Languages Syst. 16 (1994) 259–303.
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.
R.P. Kurshan and M. McMillan, A structural induction theorem for processes, Proc. 8th ACM Symp. on Principles of Distributed Computing, Edmonton (1989).
L. Lamport, An Assertional Correctness Proof of a Distributed Algorithm, Sci. Comput. Programming 2 (1983) 175–206.
L. Lamport and F.B. Schneider, Pretending Atomicity, DEC SRC Rep. 44, May 1989.
R. Letz, J. Schumann, S. Bayerl and W. Bibel, SETHEO: A High-Performance Theorem Prover, Jl. of Automated Reasoning 8 (1992) 183–212.
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.
Z. Manna et al., Step: the Stanford Temporal Prover (Draft), June 1994.
J.S. Moore, Introduction to the OBDD algorithm for the ATP Community, Jl. of Automated Reasoning 12 (1994) 33–45.
G. Ricart and A.K. Agrawala, An optimal algorithm for mutual exclusion, Comm. ACM 24 (1981) 9–17 (corrigendum: Comm. ACM 24 (1981) 578).
F. Stomp and W.P. de Roever, A principle for sequential phased reasoning about distributed systems, Formal Aspects of Computing 6 (1994) 716–737.
M.Y. Vardi, P. Wolper, An Automata-Theoretic Approach To Automatic Program Verification, Proc. Symp. on Logic in Comput. Sci., Cambridge (1986) 322–331.
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.
L. Wallen, Automated Deduction in Nonclassical Logics, MIT Press, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gribomont, E.P., Rossetto, D. (1995). CAVEAT: technique and tool for computer aided verification and transformation. In: Wolper, P. (eds) Computer Aided Verification. CAV 1995. Lecture Notes in Computer Science, vol 939. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60045-0_41
Download citation
DOI: https://doi.org/10.1007/3-540-60045-0_41
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60045-9
Online ISBN: 978-3-540-49413-3
eBook Packages: Springer Book Archive