Abstract
Critical safety and liveness properties of a concurrent system can often be proven with the help of a reachability analysis of a finite state model. This type of analysis is usually implemented as a depth-first search of the product state-space of all components in the system, with each (finite state) component modeling the behavior of one asynchronously executing process. Formal verification is achieved by coupling the depth-first search with a method for identifying those states or sequences of states that violate the correctness requirements.
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
C. Courcoubetis, M. Vardi, P. Wolper, M. Yannakakis, “Memory efficient algorithms for the verification of temporal properties,” Formal Methods in Systems Design I, 1992, pp. 275–288.
D. Dolev, M. Klawe, and M. Rodeh, “An O(n log n) unidirectional distributed algorithm for extrema finding in a circle,” Journal of Algorithms, Vol 3. (1982), pp. 245–260.
P. Godefroid, “Using partial orders to improve automatic verification methods,” Proc. 2nd Workshop on Computer Aided Verification, LNCS 531, Eds. R. Kurshan and E. Clarke, New Brunswick, New Jersey, June 18–21, 1990.
P. Godefroid, P. Wolper, “A partial approach to model checking,” 6th LICS, 1991, Amsterdam, pp. 406–415.
G.J. Holzmann, “Design and Validation of Computer Protocols,” Prentice Hall, 1992.
G.J. Holzmann, P. Godefroid, and D. Pirottin, “Coverage preserving reduction strategies for reachability analysis,” Proc. IFIP, Symp. on Protocols Specification, Testing, and Verification, June 1992, Orlando, Fl. pp. 349–364.
ANSI/IEEE Standard 8802/2, Logical Link Control, ISBN 0–471–82748–7, New York, 1984.
L. Lamport, “What good is temporal logic?,” Information Processing 83: Proc. of the 9th IFIP World Computer Congress. Ed. R.E.A. Mason, Elsevier Publ., pp. 657–668.
D. Peled, “All from one, one for all — on model checking using representatives,” 5th Int. Conf. on Computer Aided Verification, Greece, 1993, LNCS 697, Springer Verlag, pp. 409–423.
D. Peled, “Combining Partial Order Reductions with On-the-fly Model Checking,” 6th Int. Conf. on Computer Aided Verification, Stanford, Ca., June 1994. LNCS 818, Springer Verlag, pp. 377–390.
A. Valmari, “A stubborn attack on state explosion,” 2nd Int. Conf. on Computer Aided Verification, Rutgers University 1990, Dimacs Series, Vol 3, pp. 25–42.
A. Valmari, “On-the-fly verification of stubborn sets,” 5th Int. Conf. on Computer Aided Verification, 1993, LNCS 697, Springer Verlag, pp. 397–408.
P. Wolper, M.Y. Vardi, and A.P. Sistla, “Reasoning about infinite computation paths,” Proceedings of 24-th IEEE symposium on the foundations of computer science, Tuscan, 1983, pp. 185–194.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Holzmann, G.J., Peled, D. (1995). An Improvement in Formal Verification. In: Hogrefe, D., Leue, S. (eds) Formal Description Techniques VII. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34878-0_13
Download citation
DOI: https://doi.org/10.1007/978-0-387-34878-0_13
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2881-0
Online ISBN: 978-0-387-34878-0
eBook Packages: Springer Book Archive