Industrial Use of Formal Methods (eBook)
314 Seiten
John Wiley & Sons (Verlag)
978-1-118-58784-3 (ISBN)
very general books on the formal technics. The purpose of this book
is to present in a single book, a return of experience on the used
of the "formal technics" (such proof and
model-checking) on industrial examples for the transportation
domain.
This book is based on the experience of people which are
completely involved in the realization and the evaluation of safety
critical system software based.
The implication of the industrialists allows to raise the
problems of confidentiality which could appear and so allow to
supply new useful information (photos, plan of architecture, real
example).
Jean-Louis Boulanger is an Independent Safety Assessor (ISA) in the railway domain for software.
Introduction xi
Jean-Louis BOULANGER
Chapter 1. SPARK - A Language and Tool-Set for
High-Integrity Software Development 1
Ian O'NEILL
1.1. Introduction 1
1.2. An overview of SPARK 2
1.3. The rationale behind SPARK 3
1.4. Industrial applications of SPARK 15
1.5. Conclusion 25
1.6. Bibliography 26
Chapter 2. Model-Based Testing Automatic Generation of Test
Cases Using the Markov Chain Model 29
Héléne LE GUEN, Frederique VALLÉE and Anthony
FAUCOGNEY
2.1. Preliminaries on the test process 29
2.2. Modeling using Markov chains 32
2.3. The MaTeLo tool 52
2.4. Examples of industrial applications 75
2.5. Conclusion 79
2.6. Bibliography 80
Chapter 3. Safety Analysis of the Embedded Systems with the
AltaRica Approach 83
Pierre BIEBER and Christel SEGUIN
3.1. Introduction 83
3.2. Safety analysis of embedded systems 83
3.3. AltaRica language and tools 85
3.4. Examples of modeling and safety analysis 99
3.5. Comparison with other approaches 110
3.6. Conclusion 113
3.7. Special thanks 117
3.8. Bibliography 118
Chapter 4. Polyspace® 123
Patrick MUNIER
4.1. Overview 123
4.2. Introduction to software quality and verification
procedures 124
4.3. Static analysis 126
4.4. Dynamic tests 126
4.5. Abstract interpretation 127
4.6. Code verification 127
4.7. Robustness verification or contextual verification 131
4.8. Examples of Polyspace® results 133
4.9. Carrying out a code verification with Polyspace®
138
4.10. Use of Polyspace® can improve the quality of embedded
software 140
4.11. Carrying out certification with Polyspace® 145
4.12. The creation of critical onboard software 146
4.13. Concrete uses of Polyspace® 146
4.14. Conclusion 152
4.15. Bibliography 152
Chapter 5. Escher Verification Studio Perfect Developer and
Escher C Verifier 155
Judith CARLTON and David CROCKER
5.1. Introduction 155
5.2. Perfect Developer - its inspiration and foundations
156
5.3. Theoretical foundations 159
5.4. The Perfect language 160
5.5. A Perfect Developer example 161
5.6. Escher C verifier 168
5.7. The C subset supported by eCv 169
5.8. The annotation language of eCv 169
5.9. Escher C verifier examples 173
5.10. The theorem prover used by Perfect Developer and Escher C
verifier 180
5.11. Real-world applications of Perfect Developer and Escher C
verifier 181
5.12. Future work 188
5.13. Glossary 190
5.14. Bibliography 191
Chapter 6. Partial Applications of Formal Methods
195
Aryldo G. RUSSO Jr.
6.1. History 195
6.2. Case studies 196
6.3. Conclusion 212
6.4. Bibliography 213
Chapter 7. Event-B and Rodin 215
Michael BUTLER, Asieh SALEHI FATHABADI and Renato SILVA
7.1. Event-B 215
7.2. Rodin as an Event-B tool 222
7.3. Event-B model decomposition 223
7.4. Case study: metro system 225
7.5. Acknowledgments 244
7.6. Bibliography 244
Chapter 8. Conclusion 247
Jean-Louis BOULANGER
8.1. Introduction 247
8.2. Structured, semi-formal and/or formal methods 248
8.3. Conclusion 280
8.4. Bibliography 282
Glossary 287
List of Authors 293
Index 295
| Erscheint lt. Verlag | 10.5.2013 |
|---|---|
| Sprache | englisch |
| Themenwelt | Informatik ► Grafik / Design ► Digitale Bildverarbeitung |
| Mathematik / Informatik ► Informatik ► Theorie / Studium | |
| Technik ► Bauwesen | |
| Technik ► Maschinenbau | |
| Schlagworte | Industrial Engineering • Industrielle Verfahrenstechnik • Verfahrenstechnik |
| ISBN-10 | 1-118-58784-7 / 1118587847 |
| ISBN-13 | 978-1-118-58784-3 / 9781118587843 |
| Haben Sie eine Frage zum Produkt? |
EPUB (Adobe DRM)Größe: 4,2 MB
Kopierschutz: Adobe-DRM
Adobe-DRM ist ein Kopierschutz, der das eBook vor Mißbrauch schützen soll. Dabei wird das eBook bereits beim Download auf Ihre persönliche Adobe-ID autorisiert. Lesen können Sie das eBook dann nur auf den Geräten, welche ebenfalls auf Ihre Adobe-ID registriert sind.
Details zum Adobe-DRM
Dateiformat: EPUB (Electronic Publication)
EPUB ist ein offener Standard für eBooks und eignet sich besonders zur Darstellung von Belletristik und Sachbüchern. Der Fließtext wird dynamisch an die Display- und Schriftgröße angepasst. Auch für mobile Lesegeräte ist EPUB daher gut geeignet.
Systemvoraussetzungen:
PC/Mac: Mit einem PC oder Mac können Sie dieses eBook lesen. Sie benötigen eine
eReader: Dieses eBook kann mit (fast) allen eBook-Readern gelesen werden. Mit dem amazon-Kindle ist es aber nicht kompatibel.
Smartphone/Tablet: Egal ob Apple oder Android, dieses eBook können Sie lesen. Sie benötigen eine
Geräteliste und zusätzliche Hinweise
Buying eBooks from abroad
For tax law reasons we can sell eBooks just within Germany and Switzerland. Regrettably we cannot fulfill eBook-orders from other countries.
aus dem Bereich
