Coverart for item
The Resource Static Analysis of Software : The Abstract Interpretation, (electronic book)

Static Analysis of Software : The Abstract Interpretation, (electronic book)

Label
Static Analysis of Software : The Abstract Interpretation
Title
Static Analysis of Software
Title remainder
The Abstract Interpretation
Creator
Subject
Language
eng
Summary
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 working within the industry, the usual problems of confidentiality, which can occur with other books, is not an issue and so makes it possible to supply new useful information (photos, architectural plans, real examples)
Member of
Cataloging source
MiAaPQ
http://library.link/vocab/creatorName
Boulanger, Jean-Louis
Dewey number
  • 005.1/4
  • 005.14
LC call number
QA76.76.T48 S75 2011
Literary form
non fiction
Nature of contents
dictionaries
Series statement
Iste
http://library.link/vocab/subjectName
  • Computer software - Quality control
  • Computer software -- Quality control
  • Computer software - Testing
  • Computer software -- Testing
  • Debugging in computer science
Label
Static Analysis of Software : The Abstract Interpretation, (electronic book)
Instantiates
Publication
Copyright
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
  • Cover -- Title Page -- Copyright Page -- Table of Contents -- Introduction -- Chapter 1. Formal Techniques for Verification and Validation -- 1.1. Introduction -- 1.2. Realization of a software application -- 1.3. Characteristics of a software application -- 1.4. Realization cycle -- 1.4.1. Cycle in V and other realization cycles -- 1.4.2. Quality control (the impact of ISO standard 9001) -- 1.4.3. Verification and validation -- 1.5. Techniques, methods and practices -- 1.5.1. Static verification -- 1.5.2. Dynamic verification -- 1.5.3. Validation -- 1.6. New issues with verification and validation -- 1.7. Conclusion -- 1.8. Bibliography -- Chapter 2. Airbus: Formal Verification in Avionics -- 2.1. Industrial context -- 2.1.1. Avionic systems -- 2.1.2. A few examples -- 2.1.3. Regulatory framework -- 2.1.4. Avionic functions -- 2.1.5. Development of avionics levels -- 2.2. Two methods for formal verification -- 2.2.1. General principle of program proof -- 2.2.2. Static analysis by abstract interpretation -- 2.2.3. Program proof by calculation of the weakest precondition -- 2.3. Four formal verification tools -- 2.3.1. Caveat -- 2.3.2. Proof of the absence of run-time errors: Astrée -- 2.3.3. Stability and numerical precision: Fluctuat -- 2.3.4. Calculation of the worst case execution time: aiT (AbsInt GmbH) -- 2.4. Examples of industrial use -- 2.4.1. Unitary proof (verification of low level requirements) -- 2.4.2. The calculation of worst case execution time -- 2.4.3. Proof of the absence of run-time errors -- 2.5. Bibliography -- Chapter 3. Polyspace -- 3.1. Overview -- 3.2. Introduction to software quality and verification procedures -- 3.3. Static analysis -- 3.4. Dynamic tests -- 3.5. Abstract interpretation -- 3.6. Code verification -- 3.7. Robustness verification or contextual verification -- 3.7.1. Robustness verifications
  • 3.7.2. Contextual verification -- 3.8. Examples of Polyspace® results -- 3.8.1. Example of safe code -- 3.8.2. Example: dereferencing of a pointer outside its bounds -- 3.8.3. Example: inter-procedural calls -- 3.9. Carrying out a code verification with Polyspace -- 3.10. Use of Polyspace® can improve the quality of embedded software -- 3.10.1. Begin by establishing models and objectives for software quality -- 3.10.2. Example of a software quality model with objectives -- 3.10.3. Use of a subset of languages to satisfy coding rules -- 3.10.4. Use of Polyspace® to reach software quality objectives -- 3.11. Carrying out certification with Polyspace® -- 3.12. The creation of critical onboard software -- 3.13. Concrete uses of Polyspace® -- 3.13.1. Automobile: Cummins Engines improves the reliability of its motor's controllers -- 3.13.2. Aerospace: EADS guarantees the reliability of satellite launches -- 3.13.3. Medical devices: a code analysis leads to a recall of the device -- 3.13.4. Other examples of the use of Polyspace® -- 3.14. Conclusion -- 3.15. Bibliography -- Chapter 4. Software Robustness with Regards to Dysfunctional Values from Static Analysis -- 4.1. Introduction -- 4.2. Normative context -- 4.3. Elaboration of the proof of the robustness method -- 4.4. General description of the method -- 4.4.1. Required or effective value control -- 4.4.2. Computation of the required control -- 4.4.3. Verification of effective control -- 4.5. Computation of the control required -- 4.5.1. Identification of production/consumption of inputs -- 4.5.2. Computation of value domains -- 4.6. Verification of the effective control of an industrial application -- 4.6.1. Target software -- 4.6.2. Implementation -- 4.6.3. Results -- 4.7. Discussion and viewpoints -- 4.8. Conclusion -- 4.9. Bibliography
  • Chapter 5. CodePeer - Beyond Bug-finding with Static Analysis -- 5.1. Positioning of CodePeer -- 5.1.1. Mixing static checking and code understanding -- 5.1.2. Generating contracts by abstract interpretation -- 5.2. A tour of CodePeer capabilities -- 5.2.1. Find defects in code -- 5.2.2. Using annotations for code reviews -- 5.2.3. Categorization of messages -- 5.2.4. Help writing run-time tests -- 5.2.5. Different kinds of output -- 5.3. CodePeer's inner working -- 5.3.1. Overview -- 5.3.2. From Ada to SCIL -- 5.3.3. Object identification -- 5.3.4. Static single assignment and global value numbering -- 5.3.5. Possible value propagation -- 5.4. Conclusions -- 5.5. Bibiliography -- Chapter 6. Formal Methods and Compliance to the DO-178C/ED-12C Standard in Aeronautics -- 6.1. Introduction -- 6.2. Principles of the DO-178/ED-12 standard -- 6.2.1. Inputs of the software development process -- 6.2.2. Prescription of objectives -- 6.3. Verification process -- 6.4. The formal methods technical supplement -- 6.4.1. Classes of formal methods -- 6.4.2. Benefits of formal methods to meet DO-178C/ED-12C objectives -- 6.4.3. Verification of the executable code at the source level -- 6.4.4. Revision of the role of structural coverage -- 6.4.5. Verification of the completeness of requirements and detection of unintended functions -- 6.5. LLR verification by model-checking -- 6.6. Contribution to the verification of robustness properties with Frama-C -- 6.6.1. Introduction to Frama-C -- 6.6.2. Presentation of the case study -- 6.6.3. Analysis process of the case study -- 6.6.4. Conclusion on the case study -- 6.7. Static analysis and preservation of properties -- 6.8. Conclusion and perspectives -- 6.9. Appendices -- 6.9.1. Automatically annotating a source code -- 6.9.2. Automatically subdividing input intervals
  • 6.9.3. Introducing cut strategies for deductive verification -- 6.9.4. Combining abstract interpretation, deductive verification and functions which can be evaluated in assertions -- 6.9.5. Validating ACSL lemmas by formal calculus -- 6.9.6. Combining static and dynamic analysis -- 6.9.7. Finalizing -- 6.10. Acknowledgements -- 6.11. Bibliography -- Chapter 7. Efficient Method Developed by Thales for Safety Evaluation of Real-to-Integer Discretization and Overflows in SIL4 Software -- 7.1. Introduction -- 7.2. Discretization errors in the embedded code production chain -- 7.2.1. Presentation of the issue -- 7.2.2. Objective of the analysis of the real-to-integer discretization -- 7.3. Modeling of the creation and propagation of uncertainties -- 7.3.1. Creation of uncertainties -- 7.3.2. Propagation of uncertainties -- 7.4. Good practice of an analysis of real-to-integer discretization -- 7.4.1. Code extraction -- 7.4.2. Functional code reorganisation -- 7.4.3. Algorithmic breakdown in basic arithmetic relations -- 7.4.4. Computation of uncertainties -- 7.5. Arithmetic overflow and division by zero -- 7.5.1. Analysis of arithmetic overflow risk -- 7.5.2. Analysis of the risk of division by zero -- 7.6. Application to a rail signalling example -- 7.6.1. General presentation of the communication-based train controller system -- 7.6.2. Example of analysis of the behavior of speed control -- 7.6.3. Industrial scale view: a few numbers -- 7.7. Conclusion -- 7.8. Annexe: proof supplements -- 7.8.1. Proof 1: existence and unicity of integer division -- 7.8.2. Proof 2: framing the error of integer division -- 7.8.3. Proof 3: rules of the arithmetic of uncertainty intervals -- 7.8.4. Proof 4: framing of uncertainties from a product -- 7.9. Bibliography -- Conclusion and Viewpoints -- Glossary -- List of Authors -- Index
Control code
EBC1124674
Dimensions
unknown
Edition
1st ed.
Extent
1 online resource (347 pages)
Form of item
online
Isbn
9781848213203
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Note
Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2016. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries.
Reproduction note
Electronic resource.
Sound
unknown sound
Specific material designation
remote
Label
Static Analysis of Software : The Abstract Interpretation, (electronic book)
Publication
Copyright
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
  • Cover -- Title Page -- Copyright Page -- Table of Contents -- Introduction -- Chapter 1. Formal Techniques for Verification and Validation -- 1.1. Introduction -- 1.2. Realization of a software application -- 1.3. Characteristics of a software application -- 1.4. Realization cycle -- 1.4.1. Cycle in V and other realization cycles -- 1.4.2. Quality control (the impact of ISO standard 9001) -- 1.4.3. Verification and validation -- 1.5. Techniques, methods and practices -- 1.5.1. Static verification -- 1.5.2. Dynamic verification -- 1.5.3. Validation -- 1.6. New issues with verification and validation -- 1.7. Conclusion -- 1.8. Bibliography -- Chapter 2. Airbus: Formal Verification in Avionics -- 2.1. Industrial context -- 2.1.1. Avionic systems -- 2.1.2. A few examples -- 2.1.3. Regulatory framework -- 2.1.4. Avionic functions -- 2.1.5. Development of avionics levels -- 2.2. Two methods for formal verification -- 2.2.1. General principle of program proof -- 2.2.2. Static analysis by abstract interpretation -- 2.2.3. Program proof by calculation of the weakest precondition -- 2.3. Four formal verification tools -- 2.3.1. Caveat -- 2.3.2. Proof of the absence of run-time errors: Astrée -- 2.3.3. Stability and numerical precision: Fluctuat -- 2.3.4. Calculation of the worst case execution time: aiT (AbsInt GmbH) -- 2.4. Examples of industrial use -- 2.4.1. Unitary proof (verification of low level requirements) -- 2.4.2. The calculation of worst case execution time -- 2.4.3. Proof of the absence of run-time errors -- 2.5. Bibliography -- Chapter 3. Polyspace -- 3.1. Overview -- 3.2. Introduction to software quality and verification procedures -- 3.3. Static analysis -- 3.4. Dynamic tests -- 3.5. Abstract interpretation -- 3.6. Code verification -- 3.7. Robustness verification or contextual verification -- 3.7.1. Robustness verifications
  • 3.7.2. Contextual verification -- 3.8. Examples of Polyspace® results -- 3.8.1. Example of safe code -- 3.8.2. Example: dereferencing of a pointer outside its bounds -- 3.8.3. Example: inter-procedural calls -- 3.9. Carrying out a code verification with Polyspace -- 3.10. Use of Polyspace® can improve the quality of embedded software -- 3.10.1. Begin by establishing models and objectives for software quality -- 3.10.2. Example of a software quality model with objectives -- 3.10.3. Use of a subset of languages to satisfy coding rules -- 3.10.4. Use of Polyspace® to reach software quality objectives -- 3.11. Carrying out certification with Polyspace® -- 3.12. The creation of critical onboard software -- 3.13. Concrete uses of Polyspace® -- 3.13.1. Automobile: Cummins Engines improves the reliability of its motor's controllers -- 3.13.2. Aerospace: EADS guarantees the reliability of satellite launches -- 3.13.3. Medical devices: a code analysis leads to a recall of the device -- 3.13.4. Other examples of the use of Polyspace® -- 3.14. Conclusion -- 3.15. Bibliography -- Chapter 4. Software Robustness with Regards to Dysfunctional Values from Static Analysis -- 4.1. Introduction -- 4.2. Normative context -- 4.3. Elaboration of the proof of the robustness method -- 4.4. General description of the method -- 4.4.1. Required or effective value control -- 4.4.2. Computation of the required control -- 4.4.3. Verification of effective control -- 4.5. Computation of the control required -- 4.5.1. Identification of production/consumption of inputs -- 4.5.2. Computation of value domains -- 4.6. Verification of the effective control of an industrial application -- 4.6.1. Target software -- 4.6.2. Implementation -- 4.6.3. Results -- 4.7. Discussion and viewpoints -- 4.8. Conclusion -- 4.9. Bibliography
  • Chapter 5. CodePeer - Beyond Bug-finding with Static Analysis -- 5.1. Positioning of CodePeer -- 5.1.1. Mixing static checking and code understanding -- 5.1.2. Generating contracts by abstract interpretation -- 5.2. A tour of CodePeer capabilities -- 5.2.1. Find defects in code -- 5.2.2. Using annotations for code reviews -- 5.2.3. Categorization of messages -- 5.2.4. Help writing run-time tests -- 5.2.5. Different kinds of output -- 5.3. CodePeer's inner working -- 5.3.1. Overview -- 5.3.2. From Ada to SCIL -- 5.3.3. Object identification -- 5.3.4. Static single assignment and global value numbering -- 5.3.5. Possible value propagation -- 5.4. Conclusions -- 5.5. Bibiliography -- Chapter 6. Formal Methods and Compliance to the DO-178C/ED-12C Standard in Aeronautics -- 6.1. Introduction -- 6.2. Principles of the DO-178/ED-12 standard -- 6.2.1. Inputs of the software development process -- 6.2.2. Prescription of objectives -- 6.3. Verification process -- 6.4. The formal methods technical supplement -- 6.4.1. Classes of formal methods -- 6.4.2. Benefits of formal methods to meet DO-178C/ED-12C objectives -- 6.4.3. Verification of the executable code at the source level -- 6.4.4. Revision of the role of structural coverage -- 6.4.5. Verification of the completeness of requirements and detection of unintended functions -- 6.5. LLR verification by model-checking -- 6.6. Contribution to the verification of robustness properties with Frama-C -- 6.6.1. Introduction to Frama-C -- 6.6.2. Presentation of the case study -- 6.6.3. Analysis process of the case study -- 6.6.4. Conclusion on the case study -- 6.7. Static analysis and preservation of properties -- 6.8. Conclusion and perspectives -- 6.9. Appendices -- 6.9.1. Automatically annotating a source code -- 6.9.2. Automatically subdividing input intervals
  • 6.9.3. Introducing cut strategies for deductive verification -- 6.9.4. Combining abstract interpretation, deductive verification and functions which can be evaluated in assertions -- 6.9.5. Validating ACSL lemmas by formal calculus -- 6.9.6. Combining static and dynamic analysis -- 6.9.7. Finalizing -- 6.10. Acknowledgements -- 6.11. Bibliography -- Chapter 7. Efficient Method Developed by Thales for Safety Evaluation of Real-to-Integer Discretization and Overflows in SIL4 Software -- 7.1. Introduction -- 7.2. Discretization errors in the embedded code production chain -- 7.2.1. Presentation of the issue -- 7.2.2. Objective of the analysis of the real-to-integer discretization -- 7.3. Modeling of the creation and propagation of uncertainties -- 7.3.1. Creation of uncertainties -- 7.3.2. Propagation of uncertainties -- 7.4. Good practice of an analysis of real-to-integer discretization -- 7.4.1. Code extraction -- 7.4.2. Functional code reorganisation -- 7.4.3. Algorithmic breakdown in basic arithmetic relations -- 7.4.4. Computation of uncertainties -- 7.5. Arithmetic overflow and division by zero -- 7.5.1. Analysis of arithmetic overflow risk -- 7.5.2. Analysis of the risk of division by zero -- 7.6. Application to a rail signalling example -- 7.6.1. General presentation of the communication-based train controller system -- 7.6.2. Example of analysis of the behavior of speed control -- 7.6.3. Industrial scale view: a few numbers -- 7.7. Conclusion -- 7.8. Annexe: proof supplements -- 7.8.1. Proof 1: existence and unicity of integer division -- 7.8.2. Proof 2: framing the error of integer division -- 7.8.3. Proof 3: rules of the arithmetic of uncertainty intervals -- 7.8.4. Proof 4: framing of uncertainties from a product -- 7.9. Bibliography -- Conclusion and Viewpoints -- Glossary -- List of Authors -- Index
Control code
EBC1124674
Dimensions
unknown
Edition
1st ed.
Extent
1 online resource (347 pages)
Form of item
online
Isbn
9781848213203
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Note
Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2016. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries.
Reproduction note
Electronic resource.
Sound
unknown sound
Specific material designation
remote

Library Locations

Processing Feedback ...