Formal Methods (PDF)

Although formal analysis programming techniques may be quite
old, the introduction of formal methods only dates from the 1980s.
These techniques enable us to analyze the behavior of a software
application, described in a programming language. It took until the
end of the 1990s before formal methods or the B method could be
implemented in industrial applications or be usable in an
industrial setting.

Current literature only gives students and researchers very general
overviews of formal methods. The purpose of this book is to present
feedback from experience on the use of "formal methods"
(such as proof and model-checking) in industrial examples within
the transportation domain.

This book is based on the experience of people who are currently
involved in the creation and evaluation of safety critical system
software. The involvement of people from within the industry allows
us to avoid the usual problems of confidentiality which could arise
and thus enables us to supply new useful information (photos,
architecture plans, real examples, etc.).

Topics covered by the chapters of this book include SAET-METEOR,
the B method and B tools, model-based design using Simulink, the
Simulink design verifier proof tool, the implementation and
applications of SCADE (Safety Critical Application Development
Environment), GATeL: A V&V Platform for SCADE models and
ControlBuild.

Contents

1. From Classic Languages to Formal Methods, Jean-Louis
Boulanger.

2. Formal Method in the Railway Sector & #8232;the First Complex
Application: SAET-METEOR, Jean-Louis Boulanger.

3. The B Method and B Tools, Jean-Louis Boulanger.

4. Model-Based Design Using Simulink - Modeling, Code
Generation, Verification, and Validation, Mirko Conrad and Pieter
J. Mosterman.

5. Proving Global Properties with the Aid of the SIMULINK DESIGN
VERIFIER Proof Tool, Véronique Delebarre and
Jean-Frédéric Etienne.

6. SCADE: Implementation and Applications, Jean-Louis Camus.

7. GATeL: A V&V Platform for SCADE Models, Bruno Marre,
Benjamin Bianc, Patricia Mouy and Christophe Junke.

8. ControlBuild, a Development Framework & #8232;for Control
Engineering, Franck Corbier.

9. Conclusion, Jean-Louis Boulanger.