Formal methods applied to complex systems : implementation of the B method / edited by Jean-Louis Boulanger.

Format:

Book

Contributor:

Boulanger, Jean-Louis, editor.

Series:

Computer engineering series.

Computer Engineering Series

Language:

English

Subjects (All):

B method (Computer science).

Formal methods (Computer science).

Physical Description:

1 online resource (512 p.)

Edition:

1st ed.

Place of Publication:

London, England ; Hoboken, New Jersey : iSTE : Wiley, 2014.

Language Note:

English

Summary:

This book presents real-world examples of formal techniques in an industrial context. It covers formal methods such as SCADE and/or the B Method, in various fields such as railways, aeronautics, and the automotive industry. The purpose of this book is to present a summary of experience on the use of "formal methods" (based on formal techniques such as proof, abstract interpretation and model-checking) in industrial examples of complex systems, based on the experience of people currently involved in the creation and assessment of safety critical system software. The involvement of people from

Contents:

Cover; Title Page; Copyright; Contents; Introduction; Chapter 1: Presentation of the B Method ; 1.1. Introduction; 1.2. The B method; 1.2.1. Presentation; 1.2.2. The concept of an abstract machine; 1.2.2.1. Abstract machine; 1.2.2.2. Declarative part; 1.2.2.3. Composition part; 1.2.2.4. Executive part; 1.2.3. From machines to implementations; 1.2.3.1. Principle; 1.2.3.2. Refinement; 1.2.3.3. Process; 1.3. Verification and validation (V&V); 1.3.1. Internal verification; 1.3.1.1. Principles; 1.3.1.2. Syntactic and semantic analysis; 1.3.1.3. Generation of proof obligations

1.3.2. Validation or external verification1.4. Methodology; 1.4.1. Development by layer; 1.4.2. Role of the breakdown in the makeup of the POs; 1.4.3. Development cycle of a B project; 1.5. Feedback based on experience; 1.5.1. A few figures; 1.5.2. Some uses; 1.5.2.1. The current situation; 1.5.2.2. SAET-METEOR; 1.5.2.3. VAL CdG; 1.5.2.4. Eurobalise coder; 1.6. Conclusion; 1.7. Glossary; 1.8. Bibliography; Chapter 2: Atelier B; 2.1. Introduction; 2.2. Automatic refinement; 2.3. Code generation; 2.4. Proof and model animation; 2.5. The move toward open source; 2.6. Glossary; 2.7. Bibliography

Chapter 3: B Tools3.1. Introduction; 3.2. General principles; 3.3. Atelier B; 3.3.1. Project management; 3.3.2. Typechecking and PO generation; 3.3.2.1. Typechecking; 3.3.2.2. PO generation; 3.3.3. Code generation; 3.3.3.1. Verification of B0; 3.3.3.2. Code generation; 3.3.4. Prover; 3.3.4.1. Automatic prover; 3.3.4.2. Principles of proof in interactive mode; 3.3.4.3. Implementation of proof in interactive mode; 3.3.5. Tool qualification; 3.4. Open source tools; 3.4.1. Presentation; 3.4.2. ABTools; 3.4.2.1. Presentation; 3.4.2.2. The ANTLR compiler generator; 3.4.2.3. The ABTools environment

3.4.2.3.1. Presentation3.4.2.3.2. Lexical and syntactic analysis; 3.4.2.3.3. Tree manipulation; 3.4.2.3.4. Generation of POs; 3.4.2.4. Scalability; 3.4.2.4.1. Classic B; 3.4.2.4.2. B Prime; 3.4.2.4.3. System B; 3.4.2.4.4. Event B; 3.4.2.5. Results; 3.5. Conclusion; 3.6. Glossary; 3.7. Bibliography; Chapter 4: The B Method at Siemens; 4.1. Introduction; 4.1.1. Siemens Industry Mobility; 4.1.2. The CBTC system3; 4.1.3. Characteristics of B programs; 4.1.4. The target calculator; 4.2. The development process using B; 4.2.1. Development; 4.2.2. Informal specification

4.2.3. Formalization of the specification4.2.3.1. General principles; 4.2.3.2. Cutting machines; 4.2.3.3. Architecture of the abstract model and the decomposition approach; 4.2.4. Refinement and coding; 4.2.4.1. General principles; 4.2.4.2. Stages in the refinement process; 4.2.4.3. Loops and abstract iteration; 4.2.4.4. Data refinement; 4.2.5. Proof; 4.2.5.1. General principles; 4.2.5.2. Proof in practice; 4.2.5.3. Ease of proof; 4.3. Monitoring; 4.3.1. Development review; 4.3.1.1. Review objectives; 4.3.1.2. Initiation criteria; 4.3.2. Testing; 4.3.3. Safety validation

4.3.3.1. Specification analysis

Notes:

Description based upon print version of record.

Includes bibliographical references and index.

Description based on print version record.

ISBN:

9781119002925

1119002923

9781119002727

1119002729

9781119002680

1119002680

OCLC:

887825577