Compositional verification by model checking for counter-examples
- 1 May 1996
- proceedings article
- Published by Association for Computing Machinery (ACM)
- Vol. 21 (3) , 224-238
- https://doi.org/10.1145/229000.226321
Abstract
Many concurrent systems are required to maintain certain safety and liveness properties. One emerging method of achieving confidence in such systems is to statically verify them using We have developed a compositional method that directly addresses this problem in the context of multi-tasking programs. Our solution depends on three key space-saving ingredients: (1) checking for counter-examples, which leads to simpler search algorithms; (2) automatic extraction of interfaces, which allows a refinement of the finite model --- even before its communicating partners have been compiled; and (3) using propositional "strengthening assertions" for the sole purpose of reducing state space.In this paper we present our compositional approach, and describe the software tools that support it.Keywords
This publication has 6 references indexed in Scilit:
- Enhancing compositional reachability analysis with context constraintsPublished by Association for Computing Machinery (ACM) ,1993
- A layered approach to automating the verification of real-time systemsIEEE Transactions on Software Engineering, 1992
- Compositional reachability analysis using process algebraPublished by Association for Computing Machinery (ACM) ,1991
- Tableau-based model checking in the propositional mu-calculusActa Informatica, 1990
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- “Sometimes” and “not never” revisitedJournal of the ACM, 1986