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.

Doron Peled

Formal methods deal with enhancing systems reliability. Employing formal methods in hardware design has been quite successful. Applying them to software development imposes additional challenges for several reasons:

• Software systems, in general, lack the standardization of hardware systems. There is no uniformity, as everyone has his/her own favorite programming language, operating system and set of tools. On top of that, many software systems consist of several non-homogeneous parts.

• With memory costs dropping considerably every year, there is a diminishing tendency to structure and optimize code. The size of the systems and the lack of standardization usually force a manual stage of modeling and abstracting before tools and techniques can be applied. This consumes time, allow potential modeling errors, and in many cases limits the use formal methods to trained experts.

• Concurrent software systems usually involve asynchronous behavior. This makes them more intricate to model and verify.

Various successful examples demonstrate several promising directions for software verification. The magnitude of the problem suggests that it should be attacked from fresh directions:

• Guiding software development using formal methods. Due to the size of the problem, applying formal methods at the end of the development might be of limited success. It is easier and more practical to find design errors at earlier stages. Formal methods should accompany the process of software development along its various stages. At distinct stages such as features design and coding, different methods should be used.

  For example, at the very start of the design, the features of the system may be represented using message sequence charts. Tools for manipulating message sequence charts can automatically search for inconsistencies such as race conditions, or check the design for missing features. At later stages, a more detailed design can be modeled and algorithmically or manually verified against various specifications. Although a great deal of research was done at finding problems in later stages, it seems that not a lot of attention was made so far to much earlier stages, when finding problems is less costly, and more effective.

• Developing methods and models that allow exploiting special structure in the target system. Certain families of systems enjoy special structure, which can be exploited to reduce the state space explosion inherent in automatic verification. It is beneficial to use models that allow extracting this structural information, and verification methods that can exploit it. Such techniques can help scale up the applicability of formal methods to bigger, more complicated systems. In some cases, a combination of related models is required; the ability to shift between related models with complementary benefits can allow one to enjoy the best of both worlds.

  Interleaving sequences (total orders) lend themselves to convenient manipulation using automata theory. It is thus not surprising that the interleaving semantics is most popular in modeling concurrent software systems. Another way to model concurrent systems is using partial orders, modeling the causal order between the execution of events. The connection between the two models is that an interleaving sequence is a linearization of a partial order execution. It is often the case that the specification cannot distinguish between equivalent linearizations that represent the same partial order execution. One example of a method that exploits such structural information is partial order reduction. Then, it is sufficient to generate a reduced state space, with at least one linearization per each equivalence class. Another example is symmetry reduction, which exploits inherent symmetry in the structure of the modeled systems.

• Hiding technical details of the methods from the user. The introduction of graphical tools can buffer between an external, intuitive view, and an internal, more concrete, representation. Internally, an inference engine or an efficient automata manipulation algorithm may be most appropriate to do the job; externally, the user may be more comfortable with state diagrams or message sequence charts. When a clear separation cannot be achieved, tool developers should attempt to split the work between an occasional and an expert user.

  Enforcing new notions and notation upon the user, the use of highly specialized mathematical notions and notation, or the use of a jargon popular among a small group of researchers, sometimes result in criticism regarding whether it really pays off to learn and use formal methods. On the other hand, a well designed user interface can attract the user to exploit it for his/her everyday task.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.