Although significant progress has been achieved within the academic community so far, the real impact of formal methods in industry remains limited. In the following brief review of some achievements made over the past years, we analyze some reasons which limit the implementation of formal methods in the industry and outline some issues likely to promote their use for the development of critical systems.
At the specification level, starting from conventional approaches like communicating finite state machines, real specification languages including data typing mechanisms and facilities to develop modular and hierarchical specifications, have been designed to describe complex communication architectures. More recently, the expressiveness of these languages has been enhanced by introducing new features, like the expression of time constraints, that are essential for designing critical systems.
To put these specification languages and models to work, verification techniques have been enhanced with new methods for preventing state space explosion and expressing the high-level properties to be verified (model checking). As far as testing is concerned, several studies have explored the automatic derivation of test sequences from a formal specification. This is important in practice, as it allows a posteriori to re-establish a formal relationship between an implementation and its reference formal model.
Despite the progress made, several issues make the use of formal methods for the development critical systems difficult in an industrial environment.
Among these are the likely perplexity of the potential user faced with a multitude of possible approaches, the lack of maturity of the tools available, the low level of integration of such tools in CASE environments to manage and document different specifications along the system life cycle, the lack of successful case studies that are really representative of the issues to be addressed, the lack of documentation and training, and finally the lack of efficient design methods based on formal models.
Of course, this can be more or less critical according to the goal sought by the industrial user wishing to implement formal methods. For some, the goal will primarily be the formalization of specifications to allow different design groups to communicate better on a same project. For these, the discipline imposed by the formal method and its level of abstraction will be essential features. For others, the need will be the validation of some specific mechanism within a complex system. The availability of efficient tools able to deal with the problem complexity will be a key issue. Finally, others might like to consider formal methods as a means of automating the coding phase of a complex system. The quality of the produced code, in terms of memory occupation and response time, will be a key factor in the assessment of the formal approach selected.
In view of the current situation, two specific points, which should help in deploying formal methods in the industry, are developed in the sequel.
The initial step in the design which consists in translating an informal document into a formal specification often represents the first hurdle encountered by the industrial user. This is a crucial phase as the decisions made at that point (e.g., the choice of the abstraction level) usually impact the whole design and hence the quality of the resulting product. Unfortunately, very few methods have been developed with this objective in mind. What is sometimes referred to as "the modeler's art" should be "formalized" as a set of guidelines established in accordance with the formalism used and the objective sought, as well as probably the field of applications.
Similarly, one could envisage more user-friendly notations (preferably more graphic than mathematical) devoted to a particular field of application that could then easily be translated into a more general-purpose formalism. This would allow the user to use concepts he is normally familiar with in his job, while taking advantage of the use of formal methods (e.g., validation of properties based on the underlying formalism). The formalism used would then be more transparent for the users and the tools developed for a general purpose formalism could be reused in different applications. This approach is currently being investigated at LAAS-CNRS for the design of multimedia and hypermedia systems [2].
Although numerous works have dealt with the definition of specification formalisms and the related analysis techniques, few have actually been concerned with the development of design methods relying on formal approaches. In a number of fields, by relying on general purpose formalisms allowing complex specifications to be built by functionality composition, one could envisage the definition of reusable generic specification modules that would support the design process. Such attempts should be validated by the industrial and academic communities working together on significant case studies.
In addition, it seems very unlikely that a single formal approach could meet all the needs. As a result, integrating several formalisms into a design method becomes urgent to meet the specific requirements expressed at different levels of the life cycle of a complex system. Likewise, it is equally important to integrate as soon as possible new theoretical developments in order to assess their real impact. This is, for instance, particularly true for recent developments in true concurrency semantics that propose new directions for the design of complex distributed systems based on stepwise refinement.
One may finally point out that the work conducted by the academic community is often regarded as too theoretical by the industrial users who are more interested in the industrialization of classical specification techniques. When analyzing some specific property, a researcher will often be satisfied with a simplified model providing he can formally prove the desired property (analysis based on an exhaustive verification). On the other hand, the industrial user will prefer a more realistic model from which he will only get a sufficient level of confidence about the validity of that same property (analysis based on simulation). Both communities must therefore collaborate more closely because critical systems are increasingly complex as their processing architectures are becoming more distributed, and, as a consequence, these systems are increasingly prone to design errors.