Formal Verification of Control System Software / / Pierre-Loïc Garoche.
An essential introduction to the analysis and verification of control systems softwareThe verification of control systems software is critical to a host of technologies and industries, from aeronautics and medical technology to the cars we drive-the failure of controller software can cost people the...
Saved in:
Superior document: | Title is part of eBook package: De Gruyter EBOOK PACKAGE COMPLETE 2019 English |
---|---|
VerfasserIn: | |
Place / Publishing House: | Princeton, NJ : : Princeton University Press, , [2019] ©2019 |
Year of Publication: | 2019 |
Language: | English |
Series: | Princeton Series in Applied Mathematics ;
67 |
Online Access: | |
Physical Description: | 1 online resource (232 p.) :; 79 b/w illus. |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
9780691189581 |
---|---|
ctrlnum |
(DE-B1597)514661 (OCoLC)1085493238 |
collection |
bib_alma |
record_format |
marc |
spelling |
Garoche, Pierre-Loïc, author. aut http://id.loc.gov/vocabulary/relators/aut Formal Verification of Control System Software / Pierre-Loïc Garoche. Princeton, NJ : Princeton University Press, [2019] ©2019 1 online resource (232 p.) : 79 b/w illus. text txt rdacontent computer c rdamedia online resource cr rdacarrier text file PDF rda Princeton Series in Applied Mathematics ; 67 Frontmatter -- Contents -- I. Need and Tools to Verify Critical Cyber-Physical Systems -- 1. Critical Embedded Software: Control Software Development and V&V -- 2. Formal Methods: Different Approaches for Verification -- 3. Control Systems -- II. Invariant Synthesis: Convex-optimization Based Abstract Interpretation -- 4. Definitions-Background -- 5. Invariants Synthesis via Convex Optimization: Postfixpoint Computation as Semialgebraic Constraints -- 6. Template-based Analyses and Min-policy Iteration -- III. System-level Analysis at Model and Code Level -- 7. System-level Properties as Numerical Invariants -- 8. Validation of System-level Properties at Code Level -- IV. Numerical Issues -- 9. Floating-point Semantics of Analyzed Programs -- 10. Convex Optimization and Numerical Issues -- Bibliography -- Index -- Acknowledgments restricted access http://purl.org/coar/access_right/c_16ec online access with authorization star An essential introduction to the analysis and verification of control systems softwareThe verification of control systems software is critical to a host of technologies and industries, from aeronautics and medical technology to the cars we drive-the failure of controller software can cost people their lives. In this authoritative and accessible book, Pierre-Loïc Garoche provides control engineers and computer scientists with an indispensable introduction to the formal techniques for analyzing and verifying this important class of software.Too often, control engineers are unaware of the issues surrounding the verification of software, while computer scientists tend to be unfamiliar with the specificities of controller software. Garoche provides a unified approach especially geared to graduate students in both fields, covering formal verification methods as well as the design and verification of controllers. He presents a wealth of new verification techniques for performing exhaustive analysis of controller software. These include new means to compute nonlinear invariants, the use of convex optimization tools, and methods for dealing with numerical imprecisions such as floating point computations occurring in the analyzed software.As the autonomy of these systems continues to increase-such as in autonomous cars, drones, and satellites and landers-the numerical functions in critical systems are growing ever more advanced. The techniques presented here are essential to support the formal analysis of the controller software being used in these new and emerging technologies. Issued also in print. Mode of access: Internet via World Wide Web. In English. Description based on online resource; title from PDF title page (publisher's Web site, viewed 31. Jan 2022) Automatic control Computer programs. Computer software Verification. Digital control systems. MATHEMATICS / Applied. bisacsh Title is part of eBook package: De Gruyter EBOOK PACKAGE COMPLETE 2019 English 9783110610765 Title is part of eBook package: De Gruyter EBOOK PACKAGE COMPLETE 2019 9783110664232 ZDB-23-DGG Title is part of eBook package: De Gruyter EBOOK PACKAGE Mathematics 2019 English 9783110610406 Title is part of eBook package: De Gruyter EBOOK PACKAGE Mathematics 2019 9783110606362 ZDB-23-DMA Title is part of eBook package: De Gruyter Princeton Series in Applied Mathematics eBook-Package 9783110515831 ZDB-23-PAM Title is part of eBook package: De Gruyter Princeton University Press Complete eBook-Package 2019 9783110663365 print 9780691181301 https://doi.org/10.1515/9780691189581?locatt=mode:legacy https://www.degruyter.com/isbn/9780691189581 Cover https://www.degruyter.com/document/cover/isbn/9780691189581/original |
language |
English |
format |
eBook |
author |
Garoche, Pierre-Loïc, Garoche, Pierre-Loïc, |
spellingShingle |
Garoche, Pierre-Loïc, Garoche, Pierre-Loïc, Formal Verification of Control System Software / Princeton Series in Applied Mathematics ; Frontmatter -- Contents -- I. Need and Tools to Verify Critical Cyber-Physical Systems -- 1. Critical Embedded Software: Control Software Development and V&V -- 2. Formal Methods: Different Approaches for Verification -- 3. Control Systems -- II. Invariant Synthesis: Convex-optimization Based Abstract Interpretation -- 4. Definitions-Background -- 5. Invariants Synthesis via Convex Optimization: Postfixpoint Computation as Semialgebraic Constraints -- 6. Template-based Analyses and Min-policy Iteration -- III. System-level Analysis at Model and Code Level -- 7. System-level Properties as Numerical Invariants -- 8. Validation of System-level Properties at Code Level -- IV. Numerical Issues -- 9. Floating-point Semantics of Analyzed Programs -- 10. Convex Optimization and Numerical Issues -- Bibliography -- Index -- Acknowledgments |
author_facet |
Garoche, Pierre-Loïc, Garoche, Pierre-Loïc, |
author_variant |
p l g plg p l g plg |
author_role |
VerfasserIn VerfasserIn |
author_sort |
Garoche, Pierre-Loïc, |
title |
Formal Verification of Control System Software / |
title_full |
Formal Verification of Control System Software / Pierre-Loïc Garoche. |
title_fullStr |
Formal Verification of Control System Software / Pierre-Loïc Garoche. |
title_full_unstemmed |
Formal Verification of Control System Software / Pierre-Loïc Garoche. |
title_auth |
Formal Verification of Control System Software / |
title_alt |
Frontmatter -- Contents -- I. Need and Tools to Verify Critical Cyber-Physical Systems -- 1. Critical Embedded Software: Control Software Development and V&V -- 2. Formal Methods: Different Approaches for Verification -- 3. Control Systems -- II. Invariant Synthesis: Convex-optimization Based Abstract Interpretation -- 4. Definitions-Background -- 5. Invariants Synthesis via Convex Optimization: Postfixpoint Computation as Semialgebraic Constraints -- 6. Template-based Analyses and Min-policy Iteration -- III. System-level Analysis at Model and Code Level -- 7. System-level Properties as Numerical Invariants -- 8. Validation of System-level Properties at Code Level -- IV. Numerical Issues -- 9. Floating-point Semantics of Analyzed Programs -- 10. Convex Optimization and Numerical Issues -- Bibliography -- Index -- Acknowledgments |
title_new |
Formal Verification of Control System Software / |
title_sort |
formal verification of control system software / |
series |
Princeton Series in Applied Mathematics ; |
series2 |
Princeton Series in Applied Mathematics ; |
publisher |
Princeton University Press, |
publishDate |
2019 |
physical |
1 online resource (232 p.) : 79 b/w illus. Issued also in print. |
contents |
Frontmatter -- Contents -- I. Need and Tools to Verify Critical Cyber-Physical Systems -- 1. Critical Embedded Software: Control Software Development and V&V -- 2. Formal Methods: Different Approaches for Verification -- 3. Control Systems -- II. Invariant Synthesis: Convex-optimization Based Abstract Interpretation -- 4. Definitions-Background -- 5. Invariants Synthesis via Convex Optimization: Postfixpoint Computation as Semialgebraic Constraints -- 6. Template-based Analyses and Min-policy Iteration -- III. System-level Analysis at Model and Code Level -- 7. System-level Properties as Numerical Invariants -- 8. Validation of System-level Properties at Code Level -- IV. Numerical Issues -- 9. Floating-point Semantics of Analyzed Programs -- 10. Convex Optimization and Numerical Issues -- Bibliography -- Index -- Acknowledgments |
isbn |
9780691189581 9783110610765 9783110664232 9783110610406 9783110606362 9783110515831 9783110663365 9780691181301 |
callnumber-first |
Q - Science |
callnumber-subject |
QA - Mathematics |
callnumber-label |
QA76 |
callnumber-sort |
QA 276.76 V47 |
url |
https://doi.org/10.1515/9780691189581?locatt=mode:legacy https://www.degruyter.com/isbn/9780691189581 https://www.degruyter.com/document/cover/isbn/9780691189581/original |
illustrated |
Illustrated |
dewey-hundreds |
000 - Computer science, information & general works |
dewey-tens |
000 - Computer science, knowledge & systems |
dewey-ones |
005 - Computer programming, programs & data |
dewey-full |
005.14 |
dewey-sort |
15.14 |
dewey-raw |
005.14 |
dewey-search |
005.14 |
doi_str_mv |
10.1515/9780691189581?locatt=mode:legacy |
oclc_num |
1085493238 |
work_keys_str_mv |
AT garochepierreloic formalverificationofcontrolsystemsoftware |
status_str |
n |
ids_txt_mv |
(DE-B1597)514661 (OCoLC)1085493238 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Title is part of eBook package: De Gruyter EBOOK PACKAGE COMPLETE 2019 English Title is part of eBook package: De Gruyter EBOOK PACKAGE COMPLETE 2019 Title is part of eBook package: De Gruyter EBOOK PACKAGE Mathematics 2019 English Title is part of eBook package: De Gruyter EBOOK PACKAGE Mathematics 2019 Title is part of eBook package: De Gruyter Princeton Series in Applied Mathematics eBook-Package Title is part of eBook package: De Gruyter Princeton University Press Complete eBook-Package 2019 |
is_hierarchy_title |
Formal Verification of Control System Software / |
container_title |
Title is part of eBook package: De Gruyter EBOOK PACKAGE COMPLETE 2019 English |
_version_ |
1770176300859785216 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>05895nam a22008295i 4500</leader><controlfield tag="001">9780691189581</controlfield><controlfield tag="003">DE-B1597</controlfield><controlfield tag="005">20220131112047.0</controlfield><controlfield tag="006">m|||||o||d||||||||</controlfield><controlfield tag="007">cr || ||||||||</controlfield><controlfield tag="008">220131t20192019nju fo d z eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">9780691189581</subfield></datafield><datafield tag="024" ind1="7" ind2=" "><subfield code="a">10.1515/9780691189581</subfield><subfield code="2">doi</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(DE-B1597)514661</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)1085493238</subfield></datafield><datafield tag="040" ind1=" " ind2=" "><subfield code="a">DE-B1597</subfield><subfield code="b">eng</subfield><subfield code="c">DE-B1597</subfield><subfield code="e">rda</subfield></datafield><datafield tag="041" ind1="0" ind2=" "><subfield code="a">eng</subfield></datafield><datafield tag="044" ind1=" " ind2=" "><subfield code="a">nju</subfield><subfield code="c">US-NJ</subfield></datafield><datafield tag="050" ind1=" " ind2="4"><subfield code="a">QA76.76.V47</subfield></datafield><datafield tag="072" ind1=" " ind2="7"><subfield code="a">MAT003000</subfield><subfield code="2">bisacsh</subfield></datafield><datafield tag="082" ind1="0" ind2="4"><subfield code="a">005.14</subfield><subfield code="2">23</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Garoche, Pierre-Loïc, </subfield><subfield code="e">author.</subfield><subfield code="4">aut</subfield><subfield code="4">http://id.loc.gov/vocabulary/relators/aut</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Formal Verification of Control System Software /</subfield><subfield code="c">Pierre-Loïc Garoche.</subfield></datafield><datafield tag="264" ind1=" " ind2="1"><subfield code="a">Princeton, NJ : </subfield><subfield code="b">Princeton University Press, </subfield><subfield code="c">[2019]</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">©2019</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (232 p.) :</subfield><subfield code="b">79 b/w illus.</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="347" ind1=" " ind2=" "><subfield code="a">text file</subfield><subfield code="b">PDF</subfield><subfield code="2">rda</subfield></datafield><datafield tag="490" ind1="0" ind2=" "><subfield code="a">Princeton Series in Applied Mathematics ;</subfield><subfield code="v">67</subfield></datafield><datafield tag="505" ind1="0" ind2="0"><subfield code="t">Frontmatter -- </subfield><subfield code="t">Contents -- </subfield><subfield code="t">I. Need and Tools to Verify Critical Cyber-Physical Systems -- </subfield><subfield code="t">1. Critical Embedded Software: Control Software Development and V&V -- </subfield><subfield code="t">2. Formal Methods: Different Approaches for Verification -- </subfield><subfield code="t">3. Control Systems -- </subfield><subfield code="t">II. Invariant Synthesis: Convex-optimization Based Abstract Interpretation -- </subfield><subfield code="t">4. Definitions-Background -- </subfield><subfield code="t">5. Invariants Synthesis via Convex Optimization: Postfixpoint Computation as Semialgebraic Constraints -- </subfield><subfield code="t">6. Template-based Analyses and Min-policy Iteration -- </subfield><subfield code="t">III. System-level Analysis at Model and Code Level -- </subfield><subfield code="t">7. System-level Properties as Numerical Invariants -- </subfield><subfield code="t">8. Validation of System-level Properties at Code Level -- </subfield><subfield code="t">IV. Numerical Issues -- </subfield><subfield code="t">9. Floating-point Semantics of Analyzed Programs -- </subfield><subfield code="t">10. Convex Optimization and Numerical Issues -- </subfield><subfield code="t">Bibliography -- </subfield><subfield code="t">Index -- </subfield><subfield code="t">Acknowledgments</subfield></datafield><datafield tag="506" ind1="0" ind2=" "><subfield code="a">restricted access</subfield><subfield code="u">http://purl.org/coar/access_right/c_16ec</subfield><subfield code="f">online access with authorization</subfield><subfield code="2">star</subfield></datafield><datafield tag="520" ind1=" " ind2=" "><subfield code="a">An essential introduction to the analysis and verification of control systems softwareThe verification of control systems software is critical to a host of technologies and industries, from aeronautics and medical technology to the cars we drive-the failure of controller software can cost people their lives. In this authoritative and accessible book, Pierre-Loïc Garoche provides control engineers and computer scientists with an indispensable introduction to the formal techniques for analyzing and verifying this important class of software.Too often, control engineers are unaware of the issues surrounding the verification of software, while computer scientists tend to be unfamiliar with the specificities of controller software. Garoche provides a unified approach especially geared to graduate students in both fields, covering formal verification methods as well as the design and verification of controllers. He presents a wealth of new verification techniques for performing exhaustive analysis of controller software. These include new means to compute nonlinear invariants, the use of convex optimization tools, and methods for dealing with numerical imprecisions such as floating point computations occurring in the analyzed software.As the autonomy of these systems continues to increase-such as in autonomous cars, drones, and satellites and landers-the numerical functions in critical systems are growing ever more advanced. The techniques presented here are essential to support the formal analysis of the controller software being used in these new and emerging technologies.</subfield></datafield><datafield tag="530" ind1=" " ind2=" "><subfield code="a">Issued also in print.</subfield></datafield><datafield tag="538" ind1=" " ind2=" "><subfield code="a">Mode of access: Internet via World Wide Web.</subfield></datafield><datafield tag="546" ind1=" " ind2=" "><subfield code="a">In English.</subfield></datafield><datafield tag="588" ind1="0" ind2=" "><subfield code="a">Description based on online resource; title from PDF title page (publisher's Web site, viewed 31. Jan 2022)</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Automatic control</subfield><subfield code="x">Computer programs.</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Computer software</subfield><subfield code="x">Verification.</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Digital control systems.</subfield></datafield><datafield tag="650" ind1=" " ind2="7"><subfield code="a">MATHEMATICS / Applied.</subfield><subfield code="2">bisacsh</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">EBOOK PACKAGE COMPLETE 2019 English</subfield><subfield code="z">9783110610765</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">EBOOK PACKAGE COMPLETE 2019</subfield><subfield code="z">9783110664232</subfield><subfield code="o">ZDB-23-DGG</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">EBOOK PACKAGE Mathematics 2019 English</subfield><subfield code="z">9783110610406</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">EBOOK PACKAGE Mathematics 2019</subfield><subfield code="z">9783110606362</subfield><subfield code="o">ZDB-23-DMA</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">Princeton Series in Applied Mathematics eBook-Package</subfield><subfield code="z">9783110515831</subfield><subfield code="o">ZDB-23-PAM</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">Princeton University Press Complete eBook-Package 2019</subfield><subfield code="z">9783110663365</subfield></datafield><datafield tag="776" ind1="0" ind2=" "><subfield code="c">print</subfield><subfield code="z">9780691181301</subfield></datafield><datafield tag="856" ind1="4" ind2="0"><subfield code="u">https://doi.org/10.1515/9780691189581?locatt=mode:legacy</subfield></datafield><datafield tag="856" ind1="4" ind2="0"><subfield code="u">https://www.degruyter.com/isbn/9780691189581</subfield></datafield><datafield tag="856" ind1="4" ind2="2"><subfield code="3">Cover</subfield><subfield code="u">https://www.degruyter.com/document/cover/isbn/9780691189581/original</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">978-3-11-061040-6 EBOOK PACKAGE Mathematics 2019 English</subfield><subfield code="b">2019</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">978-3-11-061076-5 EBOOK PACKAGE COMPLETE 2019 English</subfield><subfield code="b">2019</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">978-3-11-066336-5 Princeton University Press Complete eBook-Package 2019</subfield><subfield code="b">2019</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_BACKALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_CL_MTPY</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_EBACKALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_EBKALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_ECL_MTPY</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_EEBKALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_ESTMALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_PPALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_STMALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">GBV-deGruyter-alles</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA12STME</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA13ENGE</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA18STMEE</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA5EBK</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">ZDB-23-DGG</subfield><subfield code="b">2019</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">ZDB-23-DMA</subfield><subfield code="b">2019</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">ZDB-23-PAM</subfield></datafield></record></collection> |