| 000 | 07578cam a2200985Ma 4500 | ||
|---|---|---|---|
| 001 | ocn828198486 | ||
| 003 | OCoLC | ||
| 005 | 20240523125535.0 | ||
| 006 | m o d | ||
| 007 | cr |n||||||||| | ||
| 008 | 111021s2012 nju ob 001 0 eng d | ||
| 010 | _z 2011039611 | ||
| 040 |
_aCDX _beng _epn _cCDX _dOCLCO _dE7B _dDG1 _dOCLCQ _dOCLCF _dOCLCQ _dEBLCP _dYDXCP _dN$T _dIDEBK _dUKDOC _dDEBSZ _dOCLCQ _dCOO _dOCLCQ _dDEBBG _dLOA _dOCLCQ _dK6U _dOCLCQ _dDG1 _dOCLCQ _dMOR _dLIP _dPIFFA _dFVL _dMERUC _dOCLCQ _dZCU _dU3W _dMERER _dCOCUF _dOCLCQ _dSTF _dWRM _dICG _dINT _dOCLCQ _dDKC _dOCLCQ _dUKAHL _dOCLCQ _dUKCRE _dOCLCO _dOCLCQ _dOCLCO _dOCLCL |
||
| 019 |
_a828298908 _a828423652 _a960203396 _a961604073 _a969531516 _a988531091 _a992013548 _a992866922 _a1005089209 _a1037728580 _a1038610812 _a1153519763 |
||
| 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 |
_aAU@ _b000054974178 |
|
| 029 | 1 |
_aCHBIS _b010026796 |
|
| 029 | 1 |
_aCHNEW _b000600427 |
|
| 029 | 1 |
_aCHNEW _b000941255 |
|
| 029 | 1 |
_aCHVBK _b480215308 |
|
| 029 | 1 |
_aDEBBG _bBV043395459 |
|
| 029 | 1 |
_aDEBBG _bBV044050057 |
|
| 029 | 1 |
_aDEBSZ _b400441179 |
|
| 029 | 1 |
_aDEBSZ _b43133921X |
|
| 029 | 1 |
_aNZ1 _b15916357 |
|
| 029 | 1 |
_aAU@ _b000066754766 |
|
| 035 |
_a(OCoLC)828198486 _z(OCoLC)828298908 _z(OCoLC)828423652 _z(OCoLC)960203396 _z(OCoLC)961604073 _z(OCoLC)969531516 _z(OCoLC)988531091 _z(OCoLC)992013548 _z(OCoLC)992866922 _z(OCoLC)1005089209 _z(OCoLC)1037728580 _z(OCoLC)1038610812 _z(OCoLC)1153519763 |
||
| 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 |
||
| 347 |
_adata file _2rda |
||
| 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�ee; 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. | ||
| 590 |
_aJohn Wiley and Sons _bWiley Online Library: Complete oBooks |
||
| 650 | 0 |
_aComputer software _xTesting. |
|
| 650 | 0 | _aDebugging in computer science. | |
| 650 | 0 |
_aComputer software _xQuality control. |
|
| 650 | 6 | _aD�ebogage. | |
| 650 | 6 |
_aLogiciels _xQualit�e _xContr�ole. |
|
| 650 | 7 |
_aCOMPUTERS _xSoftware Development & Engineering _xQuality Assurance & Testing. _2bisacsh |
|
| 650 | 7 |
_aComputer software _xQuality control _2fast |
|
| 650 | 7 |
_aComputer software _xTesting _2fast |
|
| 650 | 7 |
_aDebugging in computer science _2fast |
|
| 700 | 1 | _aBoulanger, Jean-Louis. | |
| 758 |
_ihas work: _aStatic analysis of software (Text) _1https://id.oclc.org/worldcat/entity/E39PCGDGC4TyD3jrkw4XXGmYbm _4https://id.oclc.org/worldcat/ontology/hasWork |
||
| 776 | 0 | 8 |
_iPrint version: _z9781299187788 _w(DLC) 2011039611 |
| 830 | 0 | _aISTE. | |
| 856 | 4 | 0 | _uhttps://onlinelibrary.wiley.com/doi/book/10.1002/9781118602867 |
| 938 |
_a123Library _b123L _n63995 |
||
| 938 |
_aAskews and Holts Library Services _bASKH _nAH24971852 |
||
| 938 |
_aAskews and Holts Library Services _bASKH _nAH24971856 |
||
| 938 |
_aCoutts Information Services _bCOUT _n24807255 |
||
| 938 |
_aEBL - Ebook Library _bEBLB _nEBL1124674 |
||
| 938 |
_aebrary _bEBRY _nebr10660561 |
||
| 938 |
_aEBSCOhost _bEBSC _n536709 |
||
| 938 |
_aProQuest MyiLibrary Digital eBook Collection _bIDEB _ncis24807255 |
||
| 938 |
_aYBP Library Services _bYANK _n10197093 |
||
| 938 |
_aYBP Library Services _bYANK _n10225641 |
||
| 938 |
_aYBP Library Services _bYANK _n9985044 |
||
| 994 |
_a92 _bINLUM |
||
| 999 |
_c11882 _d11882 |
||