ACM Computing Surveys 28A(4), December 1996, http://www.acm.org/surveys/1996/Formatting/. Copyright © 1996 by the Association for Computing Machinery, Inc. See the permissions statement below.

Edmund Clarke and Jeannette Wing

As computing systems continue to grow in scale and functionality, so will their complexity. As systems become more complex there is an increased likelihood of errors, some of which may cause a catastrophic loss in money, time, or even human life. The formal methods research community has long advocated that by verifying a model of a system against a set of specified properties we can gain greater assurance that the system behaves as desired. The process of formalization does not give us any absolute guarantees about correctness, but it greatly increases our understanding of the system often by revealing inconsistencies, ambiguities, and incompletenesses in its design.

In the past, the use of formal methods in practice seemed hopeless. The notations were too obscure, the techniques did not scale, and the tool support was inadequate or too hard to use. There were only a few non-trivial case studies and together they still were not convincing enough to the practicing software or hardware engineer. Few people had the training to use them effectively on the job.

Only recently have we begun to see a more promising picture for the future of formal methods. For hardware verification, industry now is adopting techniques like model checking to complement the more traditional one of simulation. For software specification, industry is open to trying out notations like Z to document a system's properties more rigorously. In both areas, researchers and practitioners are performing more and more industrial-sized case studies, and thereby gaining the benefits of using formal methods.

We believe that tools play a crucial role in the use of formal methods in practice. If a system has been described using a well-defined notation with a well-defined semantics, it is then amenable to semantic analysis through mechanical aids. Tools also help us grapple directly with the problem of scale.

Further, we believe that a partial analysis of a system is the most cost-effective way to use formal methods in practice. By "partial" we mean both analyzing a system for only some relevant set of properties and focusing our attention on only a critical part of a large system. Rather than attempt to do a complete verification of an entire system, we must content ourselves with a less ambitious, but more cost-effective, goal.

Finally, we believe that current techniques and tools for specifying and verifying systems have advanced to the point that with another "turn of the crank" partial analysis is tractable for real, industrial-sized, complex computer systems. This last claim suggests that the research community is potentially on the brink of a major breakthrough. Thus, by forging ahead we hope that we can provide the next generation of formal methods--their notations, techniques, and tool support--and that they will be used routinely by the software and hardware engineers of tomorrow.