| Introduction |
|
xi | |
|
|
|
Chapter 1 Formal Techniques for Verification and Validation |
|
|
1 | (44) |
|
|
|
|
|
1 | (1) |
|
1.2 Realization of a software application |
|
|
1 | (2) |
|
1.3 Characteristics of a software application |
|
|
3 | (1) |
|
|
|
4 | (9) |
|
1.4.1 Cycle in V and other realization cycles |
|
|
4 | (3) |
|
1.4.2 Quality control (the impact of ISO standard 9001) |
|
|
7 | (2) |
|
1.4.3 Verification and validation |
|
|
9 | (4) |
|
1.5 Techniques, methods and practices |
|
|
13 | (26) |
|
1.5.1 Static verification |
|
|
13 | (22) |
|
1.5.2 Dynamic verification |
|
|
35 | (4) |
|
|
|
39 | (1) |
|
1.6 New issues with verification and validation |
|
|
39 | (2) |
|
|
|
41 | (1) |
|
|
|
42 | (3) |
|
Chapter 2 Airbus: Formal Verification in Avionics |
|
|
45 | (68) |
|
|
|
|
|
|
|
|
|
45 | (7) |
|
|
|
45 | (1) |
|
|
|
46 | (1) |
|
2.1.3 Regulatory framework |
|
|
47 | (1) |
|
|
|
47 | (3) |
|
2.1.5 Development of avionics levels |
|
|
50 | (2) |
|
2.2 Two methods for formal verification |
|
|
52 | (14) |
|
2.2.1 General principle of program proof |
|
|
53 | (1) |
|
2.2.2 Static analysis by abstract interpretation |
|
|
54 | (7) |
|
2.2.3 Program proof by calculation of the weakest precondition |
|
|
61 | (5) |
|
2.3 Four formal verification tools |
|
|
66 | (14) |
|
|
|
66 | (2) |
|
2.3.2 Proof of the absence of run-time errors: Astree |
|
|
68 | (5) |
|
2.3.3 Stability and numerical precision: Fluctuat |
|
|
73 | (5) |
|
2.3.4 Calculation of the worst case execution time: aiT (AbsInt GmbH) |
|
|
78 | (2) |
|
2.4 Examples of industrial use |
|
|
80 | (29) |
|
2.4.1 Unitary Proof (verification of low level requirements) |
|
|
80 | (17) |
|
2.4.2 The calculation of worst case execution time |
|
|
97 | (6) |
|
2.4.3 Proof of the absence of run-time errors |
|
|
103 | (6) |
|
|
|
109 | (4) |
|
|
|
113 | (30) |
|
|
|
|
|
113 | (1) |
|
3.2 Introduction to software quality and verification procedures |
|
|
114 | (2) |
|
|
|
116 | (1) |
|
|
|
116 | (1) |
|
3.5 Abstract interpretation |
|
|
117 | (1) |
|
|
|
118 | (3) |
|
3.7 Robustness verification or contextual verification |
|
|
121 | (2) |
|
3.7.1 Robustness verifications |
|
|
122 | (1) |
|
3.7.2 Contextual verification |
|
|
122 | (1) |
|
3.8 Examples of Polyspace® results |
|
|
123 | (5) |
|
3.8.1 Example of safe code |
|
|
123 | (2) |
|
3.8.2 Example: dereferencing of a pointer outside its bounds |
|
|
125 | (1) |
|
3.8.3 Example: inter-procedural calls |
|
|
126 | (2) |
|
3.9 Carrying out a code verification with Polyspace |
|
|
128 | (2) |
|
3.10 Use of Polyspace® can improve the quality of embedded software |
|
|
130 | (5) |
|
3.10.1 Begin by establishing models and objectives for software quality |
|
|
130 | (1) |
|
3.10.2 Example of a software quality model with objectives |
|
|
130 | (2) |
|
3.10.3 Use of a subset of languages to satisfy coding rules |
|
|
132 | (1) |
|
3.10.4 Use of Polyspace® to reach software quality objectives |
|
|
133 | (2) |
|
3.11 Carrying out certification with Polyspace® |
|
|
135 | (1) |
|
3.12 The creation of critical onboard software |
|
|
135 | (1) |
|
3.13 Concrete uses of Polyspace® |
|
|
135 | (6) |
|
3.13.1 Automobile: Cummins engines improves the reliability of its motor's controllers |
|
|
136 | (1) |
|
3.13.2 Aerospace: EADS guarantees the reliability of satellite launches |
|
|
137 | (1) |
|
3.13.3 Medical devices: a code analysis leads to a recall of the device |
|
|
138 | (1) |
|
3.13.4 Other examples of the use of Polyspace® |
|
|
139 | (2) |
|
|
|
141 | (1) |
|
|
|
141 | (2) |
|
Chapter 4 Software Robustness with Regards to Dysfunctional Values from Static Analysis |
|
|
143 | (34) |
|
|
|
|
|
|
|
|
|
143 | (1) |
|
|
|
144 | (2) |
|
4.3 Elaboration of the proof of the robustness method |
|
|
146 | (5) |
|
4.4 General description of the method |
|
|
151 | (6) |
|
4.4.1 Required or effective value control |
|
|
151 | (3) |
|
4.4.2 Computation of the required control |
|
|
154 | (1) |
|
4.4.3 Verification of effective control |
|
|
155 | (2) |
|
4.5 Computation of the control required |
|
|
157 | (4) |
|
4.5.1 Identification of production/consumption of inputs |
|
|
159 | (1) |
|
4.5.2 Computation of value domains |
|
|
160 | (1) |
|
4.6 Verification of the effective control of an industrial application |
|
|
161 | (11) |
|
|
|
161 | (2) |
|
|
|
163 | (6) |
|
|
|
169 | (3) |
|
4.7 Discussion and viewpoints |
|
|
172 | (1) |
|
|
|
173 | (1) |
|
|
|
174 | (3) |
|
Chapter 5 CodePeer - Beyond Bug-finding with Static Analysis |
|
|
177 | (30) |
|
|
|
|
|
|
|
|
|
5.1 Positioning of CodePeer |
|
|
177 | (5) |
|
5.1.1 Mixing static checking and code understanding |
|
|
177 | (2) |
|
5.1.2 Generating contracts by abstract interpretation |
|
|
179 | (3) |
|
5.2 A tour of CodePeer capabilities |
|
|
182 | (6) |
|
5.2.1 Find defects in code |
|
|
182 | (2) |
|
5.2.2 Using annotations for code reviews |
|
|
184 | (2) |
|
5.2.3 Categorization of messages |
|
|
186 | (1) |
|
5.2.4 Help writing run-time tests |
|
|
187 | (1) |
|
5.2.5 Different kinds of output |
|
|
188 | (1) |
|
5.3 CodePeer's inner working |
|
|
188 | (16) |
|
|
|
188 | (3) |
|
|
|
191 | (2) |
|
5.3.3 Object identification |
|
|
193 | (2) |
|
5.3.4 Static single assignment and global value numbering |
|
|
195 | (5) |
|
5.3.5 Possible value propagation |
|
|
200 | (4) |
|
|
|
204 | (1) |
|
|
|
205 | (2) |
|
Chapter 6 Formal Methods and Compliance to the DO-178C/ED-12C Standard in Aeronautics |
|
|
207 | (66) |
|
|
|
|
|
|
|
207 | (1) |
|
6.2 Principles of the DO-178/ED-12 standard |
|
|
208 | (4) |
|
6.2.1 Inputs of the software development process |
|
|
208 | (1) |
|
6.2.2 Prescription of objectives |
|
|
209 | (3) |
|
|
|
212 | (6) |
|
6.4 The formal methods technical supplement |
|
|
218 | (11) |
|
6.4.1 Classes of formal methods |
|
|
219 | (2) |
|
6.4.2 Benefits of formal methods to meet DO-178C/ED-12C objectives |
|
|
221 | (2) |
|
6.4.3 Verification of the executable code at the source level |
|
|
223 | (2) |
|
6.4.4 Revision of the role of structural coverage |
|
|
225 | (2) |
|
6.4.5 Verification of the completeness of requirements and detection of unintended functions |
|
|
227 | (2) |
|
6.5 LLR verification by model-checking |
|
|
229 | (5) |
|
6.6 Contribution to the verification of robustness properties with Frama-C |
|
|
234 | (18) |
|
6.6.1 Introduction to Frama-C |
|
|
234 | (7) |
|
6.6.2 Presentation of the case study |
|
|
241 | (2) |
|
6.6.3 Analysis process of the case study |
|
|
243 | (9) |
|
6.6.4 Conclusion on the case study |
|
|
252 | (1) |
|
6.7 Static analysis and preservation of properties |
|
|
252 | (4) |
|
6.8 Conclusion and perspectives |
|
|
256 | (2) |
|
|
|
258 | (10) |
|
6.9.1 Automatically annotating a source code |
|
|
258 | (1) |
|
6.9.2 Automatically subdividing input intervals |
|
|
259 | (2) |
|
6.9.3 Introducing cut strategies for deductive verification |
|
|
261 | (2) |
|
6.9.4 Combining abstract interpretation, deductive verification and functions which can be evaluated in assertions |
|
|
263 | (2) |
|
6.9.5 Validating ACSL lemmas by formal calculus |
|
|
265 | (1) |
|
6.9.6 Combining static and dynamic analysis |
|
|
266 | (2) |
|
|
|
268 | (1) |
|
|
|
268 | (1) |
|
|
|
269 | (4) |
|
Chapter 7 Efficient Method Developed by Thales for Safety Evaluation of Real-to-Integer Discretization and Overflows in SIL4 Software |
|
|
273 | (46) |
|
|
|
|
|
|
|
|
|
|
|
273 | (1) |
|
7.2 Discretization errors in the embedded code production chain |
|
|
274 | (6) |
|
7.2.1 Presentation of the issue |
|
|
274 | (4) |
|
7.2.2 Objective of the analysis of the real-to-integer discretization |
|
|
278 | (2) |
|
7.3 Modeling of the creation and propagation of uncertainties |
|
|
280 | (14) |
|
7.3.1 Creation of uncertainties |
|
|
280 | (7) |
|
7.3.2 Propagation of uncertainties |
|
|
287 | (7) |
|
7.4 Good practice of an analysis of real-to-integer discretization |
|
|
294 | (3) |
|
|
|
294 | (1) |
|
7.4.2 Functional code reorganisation |
|
|
294 | (1) |
|
7.4.3 Algorithmic breakdown in basic arithmetic relations |
|
|
295 | (1) |
|
7.4.4 Computation of uncertainties |
|
|
295 | (2) |
|
7.5 Arithmetic overflow and division by zero |
|
|
297 | (2) |
|
7.5.1 Analysis of arithmetic overflow risk |
|
|
297 | (1) |
|
7.5.2 Analysis of the risk of division by zero |
|
|
298 | (1) |
|
7.6 Application to a rail signalling example |
|
|
299 | (8) |
|
7.6.1 General presentation of the communication-based train controller system |
|
|
299 | (1) |
|
7.6.2 Example of analysis of the behavior of speed control |
|
|
300 | (6) |
|
7.6.3 Industrial scale view: a few numbers |
|
|
306 | (1) |
|
|
|
307 | (1) |
|
7.8 Annexe: proof supplements |
|
|
308 | (9) |
|
7.8.1 Proof 1: existence and unicity of integer division |
|
|
308 | (4) |
|
7.8.2 Proof 2: framing the error of integer division |
|
|
312 | (2) |
|
7.8.3 Proof 3: rules of the arithmetic of uncertainty intervals |
|
|
314 | (1) |
|
7.8.4 Proof 4: framing of uncertainties from a product |
|
|
314 | (3) |
|
|
|
317 | (2) |
| Conclusion and viewpoints |
|
319 | (4) |
|
|
| Glossary |
|
323 | (4) |
| List of Authors |
|
327 | (2) |
| Index |
|
329 | |
Rohkem infot Wiley Online kohta