| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910828908603321 |
|
|
Titolo |
Formal methods applied to complex systems : implementation of the B method / / edited by Jean-Louis Boulanger |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
London, England ; ; Hoboken, New Jersey : , : iSTE : , : Wiley, , 2014 |
|
©2014 |
|
|
|
|
|
|
|
|
|
ISBN |
|
1-119-00292-3 |
1-119-00272-9 |
1-119-00268-0 |
|
|
|
|
|
|
|
|
Descrizione fisica |
|
1 online resource (512 p.) |
|
|
|
|
|
|
Collana |
|
Computer Engineering Series |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
B method (Computer science) |
Formal methods (Computer science) |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Description based upon print version of record. |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
|
Nota di contenuto |
|
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 |
|
|
|
|
|
|
Sommario/riassunto |
|
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 |
|
|
|
|
|
|
|
| |