Formal methods applied to complex systems / edited by Jean-Louis Boulanger.

Format:

Book

Contributor:

Boulanger, Jean-Louis, editor.

Series:

Computer engineering series.

Computer Engineering Series

Language:

English

Subjects (All):

Computer-aided design.

Computer engineering.

Systems engineering.

Physical Description:

1 online resource (478 p.)

Edition:

1st ed.

Place of Publication:

London, [England] ; Hoboken, New Jersey : ISTE : Wiley, 2014.

Language Note:

English

Summary:

A presentation of real examples of industrial uses for formal methods such as SCADE, the B-Method, Control Build, Matelo, etc. 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 these "formal methods" (such as proof and model-checking) in industrial examples of complex systems.It 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 usua

Contents:

Cover; Title Page ; Copyright; Contents; Introduction; Chapter 1. Formal Description and Modeling of Risks; 1.1. Introduction; 1.2. Standard process; 1.2.1. Risks, undesirable events and accidents; 1.2.2. Usual process; 1.2.3. Formal software processes for safety-critical systems; 1.2.4. Formal methods for safety-critical systems; 1.2.5. Safety kernel; 1.3. Methodology; 1.3.1. Presentation; 1.3.2. Risk mastery process; 1.4. Case study; 1.4.1. Rail transport system; 1.4.2. Presentation; 1.4.3. Description of the environment; 1.4.4. Definition of side-on collision; 1.4.5. Risk analysis

1.5. Implementation 1.5.1. The B method; 1.5.2. Implementation; 1.5.3. Specification of the rail transport system and side-on collision; 1.6. Conclusion; 1.7. Glossary; 1.8. Bibliography; Chapter 2. An Innovative Approach and an Adventure in Rail Safety; 2.1. Introduction; 2.2. Open Control of Train Interchangeable and Integrated System; 2.3. Computerized interlocking systems; 2.4. Conclusion; 2.5. Glossary; 2.6. Bibliography; Chapter 3. Use of Formal Proof for Cbtc (Octys); 3.1. Introduction; 3.2. Presentation of the Open Control of Train Interchangeable and Integrated System CBTC

3.2.1. Open Control of Train Interchangeable and Integrated System 3.2.2. Purpose of CBTC; 3.2.3. CBTC architectures; 3.3. Zone control equipment; 3.3.1. Presentation; 3.3.2. SCADE model; 3.4. Implementation of the solution; 3.5. Technical solution and implementation; 3.5.1. Property definition; 3.5.2. Two basic principles of property definition; 3.5.3. Test topologies; 3.5.4. Initial analyses; 3.5.5. The property treatment process; 3.5.6. Non-regression; 3.6. Results; 3.7. Possible improvements; 3.8. Conclusion; 3.9. Glossary; 3.10. Bibliography

Chapter 4. Safety Demonstration for A Rail Signaling Application in Nominal and Degraded Modes Using Formal Proof 4.1. Introduction; 4.1.1. Context; 4.2. Case description; 4.2.1. Operational architecture of the PMI system; 4.2.2. CIM subsystem; 4.2.3. CIM program verification with and without proof; 4.2.4. Scope of verification; 4.3. Modeling the whole system; 4.3.1. Application model; 4.3.2. Safety properties; 4.3.3. Environment model; 4.4. Formal proof suite; 4.4.1. Modeling the system; 4.4.2. Non-certified analysis chain; 4.4.3. The certified analysis chain

4.4.4. Assessment of the proof suite 4.5. Application; 4.6. Results of our experience; 4.6.1. Environment modeling; 4.6.2. Proof vs. testing; 4.6.3. Limitations; 4.7. Conclusion and prospects; 4.8. Glossary; 4.9. Bibliography; Chapter 5. Formal Verification of Data for Parameterized Systems; 5.1. Introduction; 5.1.1. Systerel; 5.1.2. Data verification; 5.1.3. Parameterized systems; 5.2. Data in the development cycle; 5.2.1. Data and property identification; 5.2.2. Modeling; 5.2.3. Property validation; 5.2.4. Data production; 5.2.5. Property verification using data; 5.2.6. Data integration

5.3. Data verification

Notes:

Description based upon print version of record.

Includes bibliographical references at the end of each chapters and index.

Description based on print version record.

ISBN:

9781119004776

1119004772

9781119004707

1119004705

9781119004844

1119004845

OCLC:

883891803