Static Analysis of Software (eBook, ePUB)
The Abstract Interpretation
Redaktion: Boulanger, Jean-Louis
Alle Infos zum eBook verschenken
Static Analysis of Software (eBook, ePUB)
The Abstract Interpretation
Redaktion: Boulanger, Jean-Louis
- Format: ePub
- Merkliste
- Auf die Merkliste
- Bewerten Bewerten
- Teilen
- Produkt teilen
- Produkterinnerung
- Produkterinnerung
Hier können Sie sich einloggen
Bitte loggen Sie sich zunächst in Ihr Kundenkonto ein oder registrieren Sie sich bei bücher.de, um das eBook-Abo tolino select nutzen zu können.
The existing literature currently available to students and researchers is very general, covering only the formal techniques of static analysis. This book presents real examples of the formal techniques called "abstract interpretation" currently being used in various industrial fields: railway, aeronautics, space, automotive, etc. The purpose of this book is to present students and researchers, in a single book, with the wealth of experience of people who are intrinsically involved in the realization and evaluation of software-based safety critical systems. As the authors are people currently…mehr
- Geräte: eReader
- mit Kopierschutz
- eBook Hilfe
- Größe: 5.41MB
Dieser Download kann aus rechtlichen Gründen nur mit Rechnungsadresse in A, B, BG, CY, CZ, D, DK, EW, E, FIN, F, GR, HR, H, IRL, I, LT, L, LR, M, NL, PL, P, R, S, SLO, SK ausgeliefert werden.
- Produktdetails
- Verlag: John Wiley & Sons
- Seitenzahl: 332
- Erscheinungstermin: 7. Februar 2013
- Englisch
- ISBN-13: 9781118602959
- Artikelnr.: 38259920
- Verlag: John Wiley & Sons
- Seitenzahl: 332
- Erscheinungstermin: 7. Februar 2013
- Englisch
- ISBN-13: 9781118602959
- Artikelnr.: 38259920
- Herstellerkennzeichnung Die Herstellerinformationen sind derzeit nicht verfügbar.
Jean-Louis Boulanger
Chapter 1. Formal Techniques for Verification and Validation 1
Jean-Louis BOULANGER
1.1. Introduction 1
1.2. Realization of a software application 1
1.3. Characteristics of a software application 3
1.4. Realization cycle 4
1.5. Techniques, methods and practices 13
1.6. New issues with verification and validation 39
1.7. Conclusion 41
1.8. Bibliography 42
Chapter 2. Airbus: Formal Verification in Avionics 45
Jean Souyris, David DELMAS and Stéphane DUPRAT
2.1. Industrial context 45
2.2. Two methods for formal verification 52
2.3. Four formal verification tools 66
2.4. Examples of industrial use 80
2.6. Bibliography 109
Chapter 3. Polyspace 113
Patrick MUNIER
3.1. Overview 113
3.2. Introduction to software quality and verification procedures 114
3.3. Static analysis 116
3.4. Dynamic tests 116
3.5. Abstract interpretation 117
3.6. Code verification 118
3.7. Robustness verification or contextual verification 121
3.8. Examples of Polyspace® results 123
3.9. Carrying out a code verification with Polyspace 128
3.10. Use of Polyspace® can improve the quality of embedded software 130
3.11. Carrying out certification with Polyspace® 135
3.12. The creation of critical onboard software 135
3.13. Concrete uses of Polyspace® 135
3.14. Conclusion 141
3.15. Bibliography 141
Chapter 4. Software Robustness with Regards to Dysfunctional Values from
Static
Analysis 143
Christèle FAURE, Jean-Louis BOULANGER and Samy AÏT KACI
4.1. Introduction 143
4.2. Normative context 144
4.3. Elaboration of the proof of the robustness method 146
4.4. General description of the method 151
4.5. Computation of the control required 157
4.6. Verification of the effective control of an industrial application 161
4.7. Discussion and viewpoints 172
4.8. Conclusion 173
4.9. Bibliography 174
Chapter 5. CodePeer - Beyond Bug-finding with Static Analysis 177
Steve BAIRD, Arnaud CHARLET, Yannick MOY and Tucker TAFT
5.1. Positioning of CodePeer 177
5.2. A tour of CodePeer capabilities 182
5.3. CodePeer's inner working 188
5.4. Conclusions 204
5.5. Bibiliography 205
Chapter 6. Formal Methods and Compliance to the DO-178C/ED-12C Standard in
Aeronautics 207
Emmanuel LEDINOT and Dillon PARIENTE
6.1. Introduction 207
6.2. Principles of the DO-178/ED-12 standard 208
6.3. Verification process 212
6.4. The formal methods technical supplement 218
6.5. LLR verification by model-checking 229
6.6. Contribution to the verification of robustness properties with Frama-C
234
6.7. Static analysis and preservation of properties 252
6.8. Conclusion and perspectives 256
6.9. Appendices 258
6.10. Acknowledgements 268
6.11. Bibliography 269
Chapter 7. Efficient Method Developed by Thales for Safety Evaluation of
Real-to-Integer Discretization and Overflows in SIL4 Software 273
Anthony BAÏOTTO, Fateh KAAKAÏ, Rafael MARCANO and Daniel DRAGO
7.1. Introduction 273
7.2. Discretization errors in the embedded code production chain 274
7.3. Modeling of the creation and propagation of uncertainties 280
7.4. Good practice of an analysis of real-to-integer discretization 294
7.5. Arithmetic overflow and division by zero 297
7.6. Application to a rail signalling example 299
7.7. Conclusion 307
7.8. Annexe: proof supplements 308
7.9. Bibliography 317
Conclusion and viewpoints 319
Jean-Louis BOULANGER
Glossary 323
List of Authors 327
Index 329
Jean-Louis Boulanger
Chapter 1. Formal Techniques for Verification and Validation 1
Jean-Louis BOULANGER
1.1. Introduction 1
1.2. Realization of a software application 1
1.3. Characteristics of a software application 3
1.4. Realization cycle 4
1.5. Techniques, methods and practices 13
1.6. New issues with verification and validation 39
1.7. Conclusion 41
1.8. Bibliography 42
Chapter 2. Airbus: Formal Verification in Avionics 45
Jean Souyris, David DELMAS and Stéphane DUPRAT
2.1. Industrial context 45
2.2. Two methods for formal verification 52
2.3. Four formal verification tools 66
2.4. Examples of industrial use 80
2.6. Bibliography 109
Chapter 3. Polyspace 113
Patrick MUNIER
3.1. Overview 113
3.2. Introduction to software quality and verification procedures 114
3.3. Static analysis 116
3.4. Dynamic tests 116
3.5. Abstract interpretation 117
3.6. Code verification 118
3.7. Robustness verification or contextual verification 121
3.8. Examples of Polyspace® results 123
3.9. Carrying out a code verification with Polyspace 128
3.10. Use of Polyspace® can improve the quality of embedded software 130
3.11. Carrying out certification with Polyspace® 135
3.12. The creation of critical onboard software 135
3.13. Concrete uses of Polyspace® 135
3.14. Conclusion 141
3.15. Bibliography 141
Chapter 4. Software Robustness with Regards to Dysfunctional Values from
Static
Analysis 143
Christèle FAURE, Jean-Louis BOULANGER and Samy AÏT KACI
4.1. Introduction 143
4.2. Normative context 144
4.3. Elaboration of the proof of the robustness method 146
4.4. General description of the method 151
4.5. Computation of the control required 157
4.6. Verification of the effective control of an industrial application 161
4.7. Discussion and viewpoints 172
4.8. Conclusion 173
4.9. Bibliography 174
Chapter 5. CodePeer - Beyond Bug-finding with Static Analysis 177
Steve BAIRD, Arnaud CHARLET, Yannick MOY and Tucker TAFT
5.1. Positioning of CodePeer 177
5.2. A tour of CodePeer capabilities 182
5.3. CodePeer's inner working 188
5.4. Conclusions 204
5.5. Bibiliography 205
Chapter 6. Formal Methods and Compliance to the DO-178C/ED-12C Standard in
Aeronautics 207
Emmanuel LEDINOT and Dillon PARIENTE
6.1. Introduction 207
6.2. Principles of the DO-178/ED-12 standard 208
6.3. Verification process 212
6.4. The formal methods technical supplement 218
6.5. LLR verification by model-checking 229
6.6. Contribution to the verification of robustness properties with Frama-C
234
6.7. Static analysis and preservation of properties 252
6.8. Conclusion and perspectives 256
6.9. Appendices 258
6.10. Acknowledgements 268
6.11. Bibliography 269
Chapter 7. Efficient Method Developed by Thales for Safety Evaluation of
Real-to-Integer Discretization and Overflows in SIL4 Software 273
Anthony BAÏOTTO, Fateh KAAKAÏ, Rafael MARCANO and Daniel DRAGO
7.1. Introduction 273
7.2. Discretization errors in the embedded code production chain 274
7.3. Modeling of the creation and propagation of uncertainties 280
7.4. Good practice of an analysis of real-to-integer discretization 294
7.5. Arithmetic overflow and division by zero 297
7.6. Application to a rail signalling example 299
7.7. Conclusion 307
7.8. Annexe: proof supplements 308
7.9. Bibliography 317
Conclusion and viewpoints 319
Jean-Louis BOULANGER
Glossary 323
List of Authors 327
Index 329