Formal Methods in Industry strongAchievementsstrong, Problems, Future.pdfVIP

Formal Methods in Industry: Achievements, Problems, Future Jean-Raymond Abrial Swiss Federal Institute of Technology Zurich jabrial@inf.ethz.ch ABSTRACT 2. FORMAL METHOD Two real projects using the B formal method are quickly The term ”formal method” used in this paper has a very presented. They show how some important parts of complex precise, and maybe narrow, meaning. It is necessary to recall systems can be developed in such a way that the outcome such a meaning here as this term is used nowadays with is ”correct by construction”. A number of factors are then many different understandings. In order to keep this paper analyzed relating the pros, the cons, and the difficulties in short, I only give the most important concepts at work in applying this approach in Industry. this usage of the B formal method. 2.1 Formal Development Categories and Subject Descriptors The B formal method used in the examples of this presen- D.2.1 [Software Engineering]: Requirements/Specifica- tation is an approach which the engineers use to transform a tions—Methodologies, Tools ; D.2.4 [Software Engineer- Software Requirement Document into some Executable Code. ing]: Software/Program Verification— Correctness proofs, So far, this does not seem to be different from what the or- Form