000 06289cam a2200793Ma 4500
001 ocn828198486
003 OCoLC
005 20230823095619.0
006 m o d
007 cr |n|||||||||
008 111021s2012 nju ob 001 0 eng d
040 _aCDX
_beng
_epn
_cCDX
_dOCLCO
_dE7B
_dDG1
_dOCLCQ
_dOCLCF
_dOCLCQ
_dEBLCP
_dYDXCP
_dN$T
_dIDEBK
_dUKDOC
_dDEBSZ
_dOCLCQ
_dCOO
_dOCLCQ
_dDEBBG
_dLOA
_dOCLCQ
019 _a828298908
_a828423652
_a960203396
_a961604073
020 _a9781118602867
_q(electronic bk.)
020 _a1118602862
_q(electronic bk.)
020 _a9781118602959
020 _a1118602951
020 _a9781118602843
_q(electronic bk.)
020 _a1118602846
_q(electronic bk.)
020 _z1848213204
020 _z9781848213203
020 _z9781299187788
020 _z1299187781
029 1 _aCHBIS
_b010026796
029 1 _aCHNEW
_b000600427
029 1 _aCHVBK
_b306236494
029 1 _aDEBBG
_bBV043395459
029 1 _aDEBSZ
_b43133921X
029 1 _aDKDLA
_b820120-katalog:000732729
029 1 _aNZ1
_b15916357
035 _a(OCoLC)828198486
_z(OCoLC)828298908
_z(OCoLC)828423652
_z(OCoLC)960203396
_z(OCoLC)961604073
037 _a450028
_bMIL
050 4 _aQA76.76.T48
_bS75 2012eb
072 7 _aCOM
_x051330
_2bisacsh
082 0 4 _a005.1/4
_223
049 _aMAIN
245 0 0 _aStatic analysis of software :
_bthe abstract interpretation /
_cedited by Jean-Louis Boulanger.
260 _aLondon, UK ;
_aHoboken, NJ :
_bISTE/Wiley,
_c2012.
300 _a1 online resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
490 1 _aISTE
504 _aIncludes bibliographical references and index.
588 0 _aPrint version record.
505 0 _aCover; 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.
505 8 _a1.8. BibliographyChapter 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.
505 8 _a2.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.
505 8 _a3.7.2. Contextual verification3.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.
505 8 _a3.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.
520 _aThe 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 curr.
650 0 _aComputer software
_xTesting.
650 0 _aDebugging in computer science.
650 0 _aComputer software
_xQuality control.
650 4 _aComputer software
_xQuality control.
650 4 _aComputer software
_xTesting.
650 4 _aDebugging in computer science.
650 7 _aCOMPUTERS
_xSoftware Development & Engineering
_xQuality Assurance & Testing.
_2bisacsh
650 7 _aComputer software
_xQuality control.
_2fast
_0(OCoLC)fst00872581
650 7 _aComputer software
_xTesting.
_2fast
_0(OCoLC)fst00872601
650 7 _aDebugging in computer science.
_2fast
_0(OCoLC)fst00888884
655 4 _aElectronic books.
700 1 _aBoulanger, Jean-Louis.
776 0 8 _iPrint version:
_z9781299187788
_w(DLC) 2011039611
830 0 _aISTE.
856 4 0 _uhttp://dx.doi.org/10.1002/9781118602867
_zWiley Online Library
994 _a92
_bDG1
999 _c20172
_d20131
526 _bswe