Research Directions for Formal Methods

Joseph Sifakis
Laboratoire VERIMAG,
Joseph.Sifakis@imag.fr,

Producing systems satisfying safety, security and quality of service requirements is an important economic stake and also a scientific and technological challenge. There is an increasing demand for methods and tools for:

• predicting/guaranteeing/evaluating the quality of the developed systems
• increasing the efficiency of developments and maintenance during lifecycle.

The application of formal methods is considered as the basis of rigorous systems development. However, the effective exploitation of these methods encounters several problems that may be explained by their inherent limitations (undecidability, intrinsic complexity), the increasing complexity of the applications, the lack of users with appropriate skills and background and finally, the lack of theoretical results.

The use of formal techniques in systems development is currently marginal. On the other hand, semi-formal and informal techniques with obvious limitations, are being extensively used in practice.
Is the state-of-the-art on formal methods mature enough to be a basis for alternative solutions?
How research on formal methods can contribute to satisfying the increasing needs in methods and tools?
How relevant are in this respect, theories, paradigms and methods considered by researchers?

Research is guided by scientific relevance even though exploitability of results is becoming an important criterion. The choice of a method depends on both its intrinsic characteristics and the concrete exploitation conditions determined by technological, economical and sociological factors. We do not expect any spectacular change in development methodologies in the foreseeable future, due to the introduction of formal techniques. The change should be rather progressive due to the transfer of only these formal methods that can be smoothly integrated in existing development environments. This means in particular, that a special effort should made for adapting formal methods to specific development methodologies and to improve their scalability and efficiency.

We believe that the following work directions are important for making formal techniques accepted and effectively used in industry:

• Development of integrated validation tools and methods allowing verification, testing and simulation. Testing is an activity of paramount economic importance which is complementary to verification and raises interesting theoretical problems. Furthermore, it has been shown that verification techniques such as model checking can be used for automatic test case generation from correct specifications. The combinatorial nature of validation problems and the high complexity of the developed systems, makes necessary the use of {\em partial} validation techniques.
• Study of development methodologies for complex systems. The top-down development paradigm is too simple to be applied to complex systems whose design is very often based on already existing solutions by reusing components, architectures or by simply extending the functionalities of existing systems by ad hoc techniques. Such an approach is the only realistic for both economical reasons (using the cumulated experience of teams) and in order to master the complexity by incremental modifications. It follows a need for languages supporting such development methodologies. The underlying semantics of object-based formalisms supporting complex data description, reusability and powerful control mechanisms are not still well understood.
• Study of requirements expression languages. There is currently a clear need for formal high level languages into which can be translated well-defined domain specific subsets of natural languages.