Industrial Use of Formal Methods: Formal VerificationJean-Louis Boulanger John Wiley & Sons, 10. mai 2013 - 314 sider At present the literature gives students and researchers of the 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). |
Innhold
Ian ONEILL | xxix |
Polyspace | 2-4 |
Partial Applications of Formal Methods | 2-6 |
EventB and Rodin | 7-27 |
Escher Verification Studio Perfect Developer | 7-28 |
ModelBased Testing Automatic Generation | 8-2 |
8-26 | |
JeanLouis BOULANGER | 8-32 |
Vanlige uttrykk og setninger
abstract interpretation aircraft allocation AltaRica model application approach architecture array automated automatically avionics platform behavior BOOL Boolean busbars CENELEC class invariant complex components context coverage data flow defined described development process division by zero doors elements embedded systems Engineering ensure environment Escher C Verifier example execution expressed failure condition fault-trees Figure formal methods formal specification functions guard implementation industrial initial input integrated interface invariants loop machine Magneti Marelli manual MaTeLo tool mathematical MathWorks node Function2 objectives occp operations output parameter Perfect Developer pointer Polyspace possible postcondition Precision Design preconditions programming language proof obligations propagation properties prove queue refinement reliability ring buffer Rodin run-time errors Safety Integrity Level SCADE schema sequence Simulink software development software quality source code SPARK standard sub-component subset techniques theorem prover train transition trns validation VeRaSiS verification conditions