IBM Logo
IBM Research Lab in Haifa
Hot Shots  
FV Research in HRL  

Download the presentation

Alessandro Cimatti

IRST - Istituto per la Ricerca Scientifica e Tecnologica
Trento, Italy


Formal Methods in the Development of Industrial Critical System

The introduction of formal methods in the development of (safety)-critical applications has many potential motivations. On one side, there is an increasing complexity of the services which can be required to computer-controlled systems. On the other hand, companies are often under the pressure of governments, regulation institutions, and even customers, which require higher and higher degrees of assurance. Some international standards strongly recommend, and even mandate, the use of formal methods for design and validation.

However, the successful introduction of formal methods in the development process is not an easy task, being it strictly conditioned by costs/benefits considerations. The crucial point is to understand how to extend an existing development process, retaining as much as possible of the current practice, but also achieving the potential advantages deriving from the use of formal methods. Issues to be tackled include are how to integrate informal and formal notations in the design, how to handle and transform large amounts of formal specifications, how to train design and development engineers to a new technology. Most often, these issues strongly depend on technical aspects of the application being developed.

The formal methods group at IRST has been directly involved in several technology transfer projects aiming at the introduction of formal techniques, model checking in particular, in the development process of industrial critical systems. In this talk will report on these experiences, discussing the difficulties tackled, the adopted solutions and the open issues.