Static analysis of software : (Record no. 11882)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 07578cam a2200985Ma 4500 |
| 001 - CONTROL NUMBER | |
| control field | ocn828198486 |
| 003 - CONTROL NUMBER IDENTIFIER | |
| control field | OCoLC |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20240523125535.0 |
| 006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS | |
| fixed length control field | m o d |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION | |
| fixed length control field | cr |n||||||||| |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 111021s2012 nju ob 001 0 eng d |
| 010 ## - LIBRARY OF CONGRESS CONTROL NUMBER | |
| Canceled/invalid LC control number | 2011039611 |
| 040 ## - CATALOGING SOURCE | |
| Original cataloging agency | CDX |
| Language of cataloging | eng |
| Description conventions | pn |
| Transcribing agency | CDX |
| Modifying agency | OCLCO |
| -- | E7B |
| -- | DG1 |
| -- | OCLCQ |
| -- | OCLCF |
| -- | OCLCQ |
| -- | EBLCP |
| -- | YDXCP |
| -- | N$T |
| -- | IDEBK |
| -- | UKDOC |
| -- | DEBSZ |
| -- | OCLCQ |
| -- | COO |
| -- | OCLCQ |
| -- | DEBBG |
| -- | LOA |
| -- | OCLCQ |
| -- | K6U |
| -- | OCLCQ |
| -- | DG1 |
| -- | OCLCQ |
| -- | MOR |
| -- | LIP |
| -- | PIFFA |
| -- | FVL |
| -- | MERUC |
| -- | OCLCQ |
| -- | ZCU |
| -- | U3W |
| -- | MERER |
| -- | COCUF |
| -- | OCLCQ |
| -- | STF |
| -- | WRM |
| -- | ICG |
| -- | INT |
| -- | OCLCQ |
| -- | DKC |
| -- | OCLCQ |
| -- | UKAHL |
| -- | OCLCQ |
| -- | UKCRE |
| -- | OCLCO |
| -- | OCLCQ |
| -- | OCLCO |
| -- | OCLCL |
| 019 ## - | |
| -- | 828298908 |
| -- | 828423652 |
| -- | 960203396 |
| -- | 961604073 |
| -- | 969531516 |
| -- | 988531091 |
| -- | 992013548 |
| -- | 992866922 |
| -- | 1005089209 |
| -- | 1037728580 |
| -- | 1038610812 |
| -- | 1153519763 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 9781118602867 |
| Qualifying information | (electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 1118602862 |
| Qualifying information | (electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 9781118602959 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 1118602951 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 9781118602843 |
| Qualifying information | (electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 1118602846 |
| Qualifying information | (electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| Canceled/invalid ISBN | 1848213204 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| Canceled/invalid ISBN | 9781848213203 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| Canceled/invalid ISBN | 9781299187788 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| Canceled/invalid ISBN | 1299187781 |
| 029 1# - OTHER SYSTEM CONTROL NUMBER (OCLC) | |
| OCLC library identifier | AU@ |
| System control number | 000054974178 |
| 029 1# - OTHER SYSTEM CONTROL NUMBER (OCLC) | |
| OCLC library identifier | CHBIS |
| System control number | 010026796 |
| 029 1# - OTHER SYSTEM CONTROL NUMBER (OCLC) | |
| OCLC library identifier | CHNEW |
| System control number | 000600427 |
| 029 1# - OTHER SYSTEM CONTROL NUMBER (OCLC) | |
| OCLC library identifier | CHNEW |
| System control number | 000941255 |
| 029 1# - OTHER SYSTEM CONTROL NUMBER (OCLC) | |
| OCLC library identifier | CHVBK |
| System control number | 480215308 |
| 029 1# - OTHER SYSTEM CONTROL NUMBER (OCLC) | |
| OCLC library identifier | DEBBG |
| System control number | BV043395459 |
| 029 1# - OTHER SYSTEM CONTROL NUMBER (OCLC) | |
| OCLC library identifier | DEBBG |
| System control number | BV044050057 |
| 029 1# - OTHER SYSTEM CONTROL NUMBER (OCLC) | |
| OCLC library identifier | DEBSZ |
| System control number | 400441179 |
| 029 1# - OTHER SYSTEM CONTROL NUMBER (OCLC) | |
| OCLC library identifier | DEBSZ |
| System control number | 43133921X |
| 029 1# - OTHER SYSTEM CONTROL NUMBER (OCLC) | |
| OCLC library identifier | NZ1 |
| System control number | 15916357 |
| 029 1# - OTHER SYSTEM CONTROL NUMBER (OCLC) | |
| OCLC library identifier | AU@ |
| System control number | 000066754766 |
| 035 ## - SYSTEM CONTROL NUMBER | |
| System control number | (OCoLC)828198486 |
| Canceled/invalid control number | (OCoLC)828298908 |
| -- | (OCoLC)828423652 |
| -- | (OCoLC)960203396 |
| -- | (OCoLC)961604073 |
| -- | (OCoLC)969531516 |
| -- | (OCoLC)988531091 |
| -- | (OCoLC)992013548 |
| -- | (OCoLC)992866922 |
| -- | (OCoLC)1005089209 |
| -- | (OCoLC)1037728580 |
| -- | (OCoLC)1038610812 |
| -- | (OCoLC)1153519763 |
| 037 ## - SOURCE OF ACQUISITION | |
| Stock number | 450028 |
| Source of stock number/acquisition | MIL |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER | |
| Classification number | QA76.76.T48 |
| Item number | S75 2012eb |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | COM |
| Subject category code subdivision | 051330 |
| Source | bisacsh |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER | |
| Classification number | 005.1/4 |
| Edition number | 23 |
| 049 ## - LOCAL HOLDINGS (OCLC) | |
| Holding library | MAIN |
| 245 00 - TITLE STATEMENT | |
| Title | Static analysis of software : |
| Remainder of title | the abstract interpretation / |
| Statement of responsibility, etc. | edited by Jean-Louis Boulanger. |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. | |
| Place of publication, distribution, etc. | London, UK ; |
| -- | Hoboken, NJ : |
| Name of publisher, distributor, etc. | ISTE/Wiley, |
| Date of publication, distribution, etc. | 2012. |
| 300 ## - PHYSICAL DESCRIPTION | |
| Extent | 1 online resource |
| 336 ## - CONTENT TYPE | |
| Content type term | text |
| Content type code | txt |
| Source | rdacontent |
| 337 ## - MEDIA TYPE | |
| Media type term | computer |
| Media type code | c |
| Source | rdamedia |
| 338 ## - CARRIER TYPE | |
| Carrier type term | online resource |
| Carrier type code | cr |
| Source | rdacarrier |
| 347 ## - DIGITAL FILE CHARACTERISTICS | |
| File type | data file |
| Source | rda |
| 490 1# - SERIES STATEMENT | |
| Series statement | ISTE |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE | |
| Bibliography, etc. note | Includes bibliographical references and index. |
| 588 0# - SOURCE OF DESCRIPTION NOTE | |
| Source of description note | Print version record. |
| 505 0# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 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. |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 1.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# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 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. |
| 505 8# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 3.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# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | 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. |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc. | 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 curr. |
| 590 ## - LOCAL NOTE (RLIN) | |
| Local note | John Wiley and Sons |
| Provenance (VM) [OBSOLETE] | Wiley Online Library: Complete oBooks |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | Computer software |
| General subdivision | Testing. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | Debugging in computer science. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | Computer software |
| General subdivision | Quality control. |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | D�ebogage. |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | Logiciels |
| General subdivision | Qualit�e |
| -- | Contr�ole. |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | COMPUTERS |
| General subdivision | Software Development & Engineering |
| -- | Quality Assurance & Testing. |
| Source of heading or term | bisacsh |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | Computer software |
| General subdivision | Quality control |
| Source of heading or term | fast |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | Computer software |
| General subdivision | Testing |
| Source of heading or term | fast |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name entry element | Debugging in computer science |
| Source of heading or term | fast |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Boulanger, Jean-Louis. |
| 758 ## - RESOURCE IDENTIFIER | |
| Relationship information | has work: |
| Label | Static analysis of software (Text) |
| Real World Object URI | https://id.oclc.org/worldcat/entity/E39PCGDGC4TyD3jrkw4XXGmYbm |
| Relationship | https://id.oclc.org/worldcat/ontology/hasWork |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY | |
| Relationship information | Print version: |
| International Standard Book Number | 9781299187788 |
| Record control number | (DLC) 2011039611 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE | |
| Uniform title | ISTE. |
| 856 40 - ELECTRONIC LOCATION AND ACCESS | |
| Uniform Resource Identifier | <a href="https://onlinelibrary.wiley.com/doi/book/10.1002/9781118602867">https://onlinelibrary.wiley.com/doi/book/10.1002/9781118602867</a> |
| 938 ## - | |
| -- | 123Library |
| -- | 123L |
| -- | 63995 |
| 938 ## - | |
| -- | Askews and Holts Library Services |
| -- | ASKH |
| -- | AH24971852 |
| 938 ## - | |
| -- | Askews and Holts Library Services |
| -- | ASKH |
| -- | AH24971856 |
| 938 ## - | |
| -- | Coutts Information Services |
| -- | COUT |
| -- | 24807255 |
| 938 ## - | |
| -- | EBL - Ebook Library |
| -- | EBLB |
| -- | EBL1124674 |
| 938 ## - | |
| -- | ebrary |
| -- | EBRY |
| -- | ebr10660561 |
| 938 ## - | |
| -- | EBSCOhost |
| -- | EBSC |
| -- | 536709 |
| 938 ## - | |
| -- | ProQuest MyiLibrary Digital eBook Collection |
| -- | IDEB |
| -- | cis24807255 |
| 938 ## - | |
| -- | YBP Library Services |
| -- | YANK |
| -- | 10197093 |
| 938 ## - | |
| -- | YBP Library Services |
| -- | YANK |
| -- | 10225641 |
| 938 ## - | |
| -- | YBP Library Services |
| -- | YANK |
| -- | 9985044 |
| 994 ## - | |
| -- | 92 |
| -- | INLUM |
No items available.