Static analysis of software : (Record no. 20172)

MARC details
000 -LEADER
fixed length control field 06289cam a2200793Ma 4500
001 - CONTROL NUMBER
control field ocn828198486
003 - CONTROL NUMBER IDENTIFIER
control field OCoLC
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20230823095619.0
006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS--GENERAL INFORMATION
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
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
019 ## -
-- 828298908
-- 828423652
-- 960203396
-- 961604073
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
ISBN 9781118602867
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
ISBN 1118602862
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
ISBN 9781118602959
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
ISBN 1118602951
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
ISBN 9781118602843
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
ISBN 1118602846
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
Cancelled/invalid ISBN 1848213204
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
Cancelled/invalid ISBN 9781848213203
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
Cancelled/invalid ISBN 9781299187788
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
Cancelled/invalid ISBN 1299187781
029 1# - (OCLC)
OCLC library identifier CHBIS
System control number 010026796
029 1# - (OCLC)
OCLC library identifier CHNEW
System control number 000600427
029 1# - (OCLC)
OCLC library identifier CHVBK
System control number 306236494
029 1# - (OCLC)
OCLC library identifier DEBBG
System control number BV043395459
029 1# - (OCLC)
OCLC library identifier DEBSZ
System control number 43133921X
029 1# - (OCLC)
OCLC library identifier DKDLA
System control number 820120-katalog:000732729
029 1# - (OCLC)
OCLC library identifier NZ1
System control number 15916357
035 ## - SYSTEM CONTROL NUMBER
System control number (OCoLC)828198486
Canceled/invalid control number (OCoLC)828298908
-- (OCoLC)828423652
-- (OCoLC)960203396
-- (OCoLC)961604073
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. (IMPRINT)
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 ## -
-- text
-- txt
-- rdacontent
337 ## -
-- computer
-- c
-- rdamedia
338 ## -
-- online resource
-- cr
-- rdacarrier
490 1# - SERIES STATEMENT
Series statement ISTE
504 ## - BIBLIOGRAPHY, ETC. NOTE
Bibliography, etc Includes bibliographical references and index.
588 0# -
-- 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ée; 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.
526 ## - STUDY PROGRAM INFORMATION NOTE
Department Software Engineering
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer software
General subdivision Testing.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Debugging in computer science.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer software
General subdivision Quality control.
650 #4 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer software
General subdivision Quality control.
650 #4 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer software
General subdivision Testing.
650 #4 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Debugging in computer science.
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as 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 as entry element Computer software
General subdivision Quality control.
Source of heading or term fast
-- (OCoLC)fst00872581
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer software
General subdivision Testing.
Source of heading or term fast
-- (OCoLC)fst00872601
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Debugging in computer science.
Source of heading or term fast
-- (OCoLC)fst00888884
655 #4 - INDEX TERM--GENRE/FORM
Genre/form data or focus term Electronic books.
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Boulanger, Jean-Louis.
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Display text 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="http://dx.doi.org/10.1002/9781118602867">http://dx.doi.org/10.1002/9781118602867</a>
Public note Wiley Online Library
994 ## -
-- 92
-- DG1

No items available.