Combining Formal Methods

  • Doron A. Peled
Part of the Texts in Computer Science book series (TCS)


Each one of the software reliability methods presented in this book has several typical advantages and disadvantages. Automatic verification methods are desirable since they are exhaustive and require minimal human intervention. However, the effectiveness of such methods decreases rapidly with the size of the checked system. Theorem proving can be applied to infinite state systems, but is slow and requires extensive human skills. Testing can be applied directly to a system, but is not comprehensive, hence may omit detecting some errors. Integrating different formal methods to work together may allow combining their strengths, while alleviating some of their weaknesses.


Model Check Formal Method Abstract Version Combine Test Simulation Relation 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Further Reading

  1. D. Lee, M. Yannakakis, Principles and methods of testing finite state machines - a survey, Proceedings of the IEEE, 84(8), 1090-1126, 1996.Google Scholar
  2. D. Peled, M.Y. Vardi, M. Yannakakis, Black box checking, Formal Methods for Protocol Engineering and Distributed Systems, Formal Methods for Protocol Engineering and Distributed Systems, 1999, Kluwer, China, 225-240.Google Scholar
  3. A.M. Stavely Toward ZeroDefect Programming, Addison-Wesley, 1999.Google Scholar

Copyright information

© Lucent Technologies 2001

Authors and Affiliations

  • Doron A. Peled
    • 1
  1. 1.Computing SciencesBell Labs/Lucent TechnologiesMurray HillUSA

Personalised recommendations