Atnaujinkite slapukų nuostatas

El. knyga: Industrial Use of Formal Methods: Formal Verification

Edited by
  • Formatas: PDF+DRM
  • Išleidimo metai: 27-Dec-2012
  • Leidėjas: ISTE Ltd and John Wiley & Sons Inc
  • Kalba: eng
  • ISBN-13: 9781118587904
Kitos knygos pagal šią temą:
Industrial Use of Formal Methods: Formal VerificationDidesnis paveikslėlis
  • Formatas: PDF+DRM
  • Išleidimo metai: 27-Dec-2012
  • Leidėjas: ISTE Ltd and John Wiley & Sons Inc
  • Kalba: eng
  • ISBN-13: 9781118587904
Kitos knygos pagal šią temą:

DRM apribojimai

  • Kopijuoti:

    neleidžiama

  • Spausdinti:

    neleidžiama

  • El. knygos naudojimas:

    Skaitmeninių teisių valdymas (DRM)
    Leidykla pateikė šią knygą šifruota forma, o tai reiškia, kad norint ją atrakinti ir perskaityti reikia įdiegti nemokamą programinę įrangą. Norint skaityti šią el. knygą, turite susikurti Adobe ID . Daugiau informacijos  čia. El. knygą galima atsisiųsti į 6 įrenginius (vienas vartotojas su tuo pačiu Adobe ID).

    Reikalinga programinė įranga
    Norint skaityti šią el. knygą mobiliajame įrenginyje (telefone ar planšetiniame kompiuteryje), turite įdiegti šią nemokamą programėlę: PocketBook Reader (iOS / Android)

    Norint skaityti šią el. knygą asmeniniame arba „Mac“ kompiuteryje, Jums reikalinga  Adobe Digital Editions “ (tai nemokama programa, specialiai sukurta el. knygoms. Tai nėra tas pats, kas „Adobe Reader“, kurią tikriausiai jau turite savo kompiuteryje.)

    Negalite skaityti šios el. knygos naudodami „Amazon Kindle“.

"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)"--

French, British, and Brazilian scholars explain formal analysis programming techniques that let developers analyze behavior of a software application that can deal with huge commercial software projects. They cover SPARK: a language and tool set for high-integrity software development, automatically generating test cases using the Markov chain model, analyzing the safety of embedded systems with the AltaRica approach, Polyspace, Escher Verification Studio Perfect Developer and Escher C Verifier, partial applications of formal methods, and Event-B and Rodin. Annotation ©2012 Book News, Inc., Portland, OR (booknews.com)

Introduction xi
Jean-Louis Boulanger
Chapter 1 SPARK - A Language and Tool-Set for High-Integrity Software Development
1(28)
Ian O'Neill
1.1 Introduction
1(1)
1.2 An overview of SPARK
2(1)
1.2.1 What is SPARK?
2(1)
1.3 The rationale behind SPARK
3(12)
1.3.1 Flow analysis
6(5)
1.3.2 Code proof
11(3)
1.3.3 Correctness by construction
14(1)
1.4 Industrial applications of SPARK
15(10)
1.4.1 SHOLIS
16(1)
1.4.2 Lockheed-Martin C-130J mission computer
17(2)
1.4.3 MULTOS CA
19(1)
1.4.4 Tokeneer
20(3)
1.4.5 Aircraft monitoring software
23(1)
1.4.6 iFACTS
24(1)
1.4.7 SPARK Skein
24(1)
1.5 Conclusion
25(1)
1.6 Bibliography
26(3)
Chapter 2 Model-Based Testing Automatic Generation of Test Cases Using the Markov Chain Model
29(54)
Helene Le Guen
Frederique Vallee
Anthony Faucogney
2.1 Preliminaries on the test process
29(3)
2.1.1 Findings
29(1)
2.1.2 Test optimization
30(1)
2.1.3 The statistical usage test
30(2)
2.1.4 Generating test cases
32(1)
2.2 Modeling using Markov chains
32(20)
2.2.1 Origin
32(2)
2.2.2 Mathematical formalization
34(8)
2.2.3 Principles of generation
42(2)
2.2.4 Some indicators
44(1)
2.2.5 Calculating reliability
45(7)
2.3 The MaTeLo tool
52(23)
2.3.1 Engineering tests directed by models, model-based testing
52(2)
2.3.2 A chain of tools
54(1)
2.3.3 The usage model
55(9)
2.3.4 Configuration of test strategies
64(1)
2.3.5 Generating test campaigns
65(4)
2.3.6 Analysis of the results and indicators
69(6)
2.4 Examples of industrial applications
75(4)
2.4.1 AUDI
75(2)
2.4.2 Magneti marelli
77(1)
2.4.3 Other industrial applications
78(1)
2.4.4 Industrialization of the tests
78(1)
2.5 Conclusion
79(1)
2.6 Bibliography
80(3)
Chapter 3 Safety Analysis of the Embedded Systems with the AltaRica Approach
83(40)
Pierre Bieber
Christel Seguin
3.1 Introduction
83(1)
3.2 Safety analysis of embedded systems
83(2)
3.3 AltaRica language and tools
85(14)
3.3.1 The AltaRica language
85(7)
3.3.2 Modeling the propagation of failures with AltaRica
92(3)
3.3.3 Tools associated with AltaRica
95(4)
3.4 Examples of modeling and safety analysis
99(11)
3.4.1 Integrated modular avionics architecture
99(5)
3.4.2 System of electric power generation and distribution
104(6)
3.5 Comparison with other approaches
110(3)
3.5.1 Some precursors
111(1)
3.5.2 Tools for preexisting formal languages
111(1)
3.5.3 Languages for physical systems
112(1)
3.5.4 Injecting faults in nominal models
112(1)
3.6 Conclusion
113(4)
3.6.1 An approach to assess the safety of systems tested in aeronautics
113(1)
3.6.2 Clarification of the system architecture and horizontal exploration of the failure propagation: impacts on the scope of analyses
113(2)
3.6.3 Clarification of the nominal system characteristics: impacts on the generic definitions of the failure modes
115(1)
3.6.4 Compositional models of failure propagation: impacts on the overall safety process
116(1)
3.7 Special thanks
117(1)
3.8 Bibliography
118(5)
Chapter 4 Polyspace®
123(32)
Patrick Munier
4.1 Overview
123(1)
4.2 Introduction to software quality and verification procedures
124(2)
4.3 Static analysis
126(1)
4.4 Dynamic tests
126(1)
4.5 Abstract interpretation
127(1)
4.6 Code verification
127(4)
4.7 Robustness verification or contextual verification
131(2)
4.7.1 Robustness verification
132(1)
4.7.2 Contextual verification
132(1)
4.8 Examples of Polyspace® results
133(5)
4.8.1 Example of safe code
133(2)
4.8.2 Example: de-referencing of a pointer outside its bounds
135(1)
4.8.3 Example: inter-procedural calls
136(2)
4.9 Carrying out a code verification with Polyspace®
138(2)
4.10 Use of Polyspace® can improve the quality of embedded software
140(5)
4.10.1 Begin by establishing models and objectives for software quality
141(1)
4.10.2 Example of a software quality model with objectives
141(1)
4.10.3 Use of a subset of languages to satisfy coding rules
142(1)
4.10.4 Use of Polyspace® to reach software quality objectives
143(2)
4.11 Carrying out certification with Polyspace®
145(1)
4.12 The creation of critical onboard software
146(1)
4.13 Concrete uses of Polyspace®
146(6)
4.13.1 Automobile: Cummins engines improve the reliability of their motors' controllers
147(1)
4.13.2 Aerospace: EADS guarantees the reliability of satellite launches
148(1)
4.13.3 Medical devices: a code analysis leads to a recall of the device
149(1)
4.13.4 Other examples of the use of Polyspace®
150(2)
4.14 Conclusion
152(1)
4.15 Bibliography
152(3)
Chapter 5 Escher Verification Studio Perfect Developer and Escher C Verifier
155(40)
Judith Carlton
David Crocker
5.1 Introduction
155(1)
5.1.1 Escher Technologies Ltd
155(1)
5.1.2 Needs
156(1)
5.2 Perfect Developer - its inspiration and foundations
156(3)
5.2.1 Design-by-Contract
156(1)
5.2.2 Verified Design-by-Contract
157(1)
5.2.3 Perfect Developer
158(1)
5.3 Theoretical foundations
159(1)
5.4 The Perfect language
160(1)
5.5 A Perfect Developer example
161(7)
5.5.1 The specification
161(3)
5.5.2 Verification conditions generated when the unrefined ring buffer is verified
164(1)
5.5.3 Refining to a ring buffer
165(3)
5.5.4 Verification conditions generated when the refined ring buffer is verified
168(1)
5.6 Escher C verifier
168(1)
5.7 The C subset supported by eCv
169(1)
5.8 The annotation language of eCv
169(4)
5.8.1 Applying verified design-by-contract to C
170(1)
5.8.2 Arrays and pointers
171(1)
5.8.3 Unions
172(1)
5.8.4 Side effects
172(1)
5.8.5 Quantifiers
173(1)
5.9 Escher C verifier examples
173(7)
5.9.1 First escher C verifier example
173(2)
5.9.2 Second example
175(5)
5.10 The theorem prover used by Perfect Developer and Escher C verifier
180(1)
5.10.1 Logic
180(1)
5.10.2 Term rewriter
180(1)
5.11 Real-world applications of Perfect Developer and Escher C verifier
181(7)
5.11.1 Safety-critical systems
181(1)
5.11.2 Teaching university classes
182(1)
5.11.3 IT system development: Precision Design Technology Ltd
182(6)
5.12 Future work
188(2)
5.12.1 Composite projects
188(1)
5.12.2 Code generation
188(1)
5.12.3 Concurrency
189(1)
5.12.4 Extension
189(1)
5.12.5 Conclusion
189(1)
5.13 Glossary
190(1)
5.14 Bibliography
191(4)
Chapter 6 Partial Applications of Formal Methods
195(20)
Aryldo G. Russo Jr.
6.1 History
195(1)
6.1.1 Context
196(1)
6.2 Case studies
196(16)
6.2.1 Early 2007 - the B method and railway domain - breaking the wall
196(1)
6.2.2 Early 2008 - requirements verification
197(4)
6.2.3 2009 - tool comparison
201(1)
6.2.4 Late 2009 - writing a formal specification - user point of view
202(3)
6.2.5 Early 2010 - a methodological approach to a B formalization
205(4)
6.2.6 Early 2011 changing the way to vital verification
209(2)
6.2.7 The VeRaSiS plug-in
211(1)
6.2.8 Results
211(1)
6.3 Conclusion
212(1)
6.4 Bibliography
213(2)
Chapter 7 Event-B and Rodin
215(32)
Michael Butler
Asieh Salehi Fathabadi
Renato Silva
7.1 Event-B
215(7)
7.1.1 The Event-B definition
215(1)
7.1.2 Event-B structure and notation
216(2)
7.1.3 Refinement in Event-B
218(2)
7.1.4 Proof obligations
220(2)
7.1.5 A comparison between Event-B and other formal methods
222(1)
7.2 Rodin as an Event-B tool
222(1)
7.3 Event-B model decomposition
223(2)
7.3.1 Overview
223(1)
7.3.2 Decomposition styles
223(2)
7.4 Case study: metro system
225(19)
7.4.1 Overview of the safety-critical metro system
226(2)
7.4.2 Abstract model: MetroSystem_M0
228(5)
7.4.3 First refinement: MetroSystem_M1
233(1)
7.4.4 Second refinement: MetroSystem_M2
234(2)
7.4.5 Third refinement and first decomposition: MetroSystem_M3
236(1)
7.4.6 Machine Track
237(2)
7.4.7 Machine Train
239(1)
7.4.8 Machine Middleware
239(1)
7.4.9 Refinement of Train: Train_M1
239(4)
7.4.10 Further development
243(1)
7.4.11 Conclusion
243(1)
7.5 Acknowledgments
244(1)
7.6 Bibliography
244(3)
Chapter 8 Conclusion
247(40)
Jean-Louis Boulanger
8.1 Introduction
247(1)
8.2 Structured, semi-formal and/or formal methods
248(32)
8.2.1 E/E/PE system
248(1)
8.2.2 Rail sector
249(3)
8.2.3 Taking into account techniques and formal methods
252(2)
8.2.4 Software requirement specification
254(12)
8.2.5 Coding
266(12)
8.2.6 Verification and validation (V&V)
278(2)
8.3 Conclusion
280(2)
8.4 Bibliography
282(5)
Glossary 287(6)
List of Authors 293(2)
Index 295
Jean-Louis Boulanger is an Independent Safety Assessor (ISA) in the railway domain for software.
Daugiau apie elektronines knygas Daugiau apie elektronines knygas
Pastovi nuoroda: https://www.kriso.lt/db/97811185879042e.html
Raktažodžiai: