UID:
almafu_9959328665002883
Format:
1 online resource
ISBN:
9781119004707
,
1119004705
,
9781119004844
,
1119004845
Series Statement:
Computer engineering series
Content:
A presentation of real examples of industrial uses for formal methods such as SCADE, the B-Method, ControlBuild, 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.
Note:
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. Implementation1.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 System3.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 Proof4.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 suite4.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.
Additional Edition:
Print version: Formal methods applied to industrial complex systems ISBN 9781848216327
Language:
English
Keywords:
Electronic books.
;
Electronic books.
;
Electronic books.
DOI:
10.1002/9781119004707
URL:
https://onlinelibrary.wiley.com/doi/book/10.1002/9781119004707
URL:
https://onlinelibrary.wiley.com/doi/book/10.1002/9781119004707
URL:
https://onlinelibrary.wiley.com/doi/book/10.1002/9781119004707
Bookmarklink
