|
|
|
|
| LEADER |
00000nam a2200000Ii 4500 |
| 001 |
b3269229 |
| 003 |
CStclU |
| 005 |
20190503173205.4 |
| 006 |
m o d |
| 007 |
cr cnu|||unuuu |
| 008 |
190212s2019 nju ob 001 0 eng d |
| 020 |
|
|
|a 9780691189581
|q (electronic bk.)
|
| 020 |
|
|
|a 0691189587
|q (electronic bk.)
|
| 020 |
|
|
|z 9780691181301
|
| 035 |
|
|
|a (NhCcYBP)ebc5695063
|
| 040 |
|
|
|a NhCcYBP
|c NhCcYBP
|
| 050 |
|
4 |
|a TJ225
|b .G37 2019
|
| 072 |
|
7 |
|a TEC
|x 009000
|2 bisacsh
|
| 082 |
0 |
4 |
|a 629.8
|2 23
|
| 100 |
1 |
|
|a Garoche, Pierre-Loïc,
|e author.
|
| 245 |
1 |
0 |
|a Formal Verification of Control System Software /
|c Pierre-Lö ıc Garoche.
|
| 264 |
|
1 |
|a Princeton, New Jersey :
|b Princeton University Press,
|c [2019]
|
| 300 |
|
|
|a 1 online resource.
|
| 336 |
|
|
|a text
|b txt
|2 rdacontent
|
| 337 |
|
|
|a computer
|b c
|2 rdamedia
|
| 338 |
|
|
|a online resource
|b cr
|2 rdacarrier
|
| 490 |
1 |
|
|a Princeton series in applied mathematics
|
| 504 |
|
|
|a Includes bibliographical references and index.
|
| 505 |
0 |
|
|a Cover; Contents; I. Need and Tools to Verify Critical Cyber-Physical Systems; 1. Critical Embedded Software: Control Software Development and V 2. Formal Methods: Different Approaches for Verification; 2.1 Semantics and Properties; 2.2 A Formal Verification Methods Overview; 2.3 Deductive Methods; 2.4 SMT-based Model-checking; 2.5 Abstract Interpretation (of Collecting Semantics); 2.6 Need for Inductive Invariants; 3. Control Systems; 3.1 Controllers' Development Process; 3.2 A Simple Linear System: Spring-mass Damper
|
| 505 |
8 |
|
|a II. Invariant Synthesis: Convex-optimization Based Abstract Interpretation4. Definitions-Background; 4.1 Discrete Dynamical Systems; 4.2 Elements of (Applied) Convex Optimization; 5. Invariants Synthesis via Convex Optimization: Postfixpoint Computation as Semialgebraic Constraints; 5.1 Invariants, Lyapunov Functions, and Convex Optimization; 5.2 Quadratic Invariants; 5.3 Piecewise Quadratic Invariants; 5.4 k-inductive Quadratic Invariants; 5.5 Polynomial Invariants; 5.6 Image Measure Method; 5.7 Related Works; 6. Template-based Analyses and Min-policy Iteration
|
| 505 |
8 |
|
|a 6.1 Template-based Abstract Domains6.2 Template Abstraction Fixpoint as an Optimization Problem; 6.3 SOS-relaxed Semantics; 6.4 Example; 6.5 Related Works; III. System-level Analysis at Model and Code Level; 7. System-level Properties as Numerical Invariants; 7.1 Open-loop and Closed-loop Stability; 7.2 Robustness with Vector Margin; 7.3 Related Work; 8. Validation of System-level Properties at Code Level; 8.1 Axiomatic Semantics of Control Properties through Synchronous Observers and Hoare Triples; 8.2 Generating Annotations: A Strongest Postcondition Propagation Algorithm
|
| 505 |
8 |
|
|a 8.3 Discharging Proof Objectives using PVSIV. Numerical Issues; 9. Floating-point Semantics of Analyzed Programs; 9.1 Floating-point Semantics; 9.2 Revisiting Inductiveness Constraints; 9.3 Bound Floating-point Errors: Taylor-based Abstractions aka Zonotopic Abstract Domains; 9.4 Related Works; 10. Convex Optimization and Numerical Issues; 10.1 Convex Optimization Algorithms; 10.2 Guaranteed Feasible Solutions with Floats; Bibliography; Index; Acknowledgments
|
| 533 |
|
|
|a Electronic reproduction.
|b Ann Arbor, MI
|n Available via World Wide Web.
|
| 588 |
0 |
|
|a Online resource; title from PDF title page (EBSCO, viewed February 13, 2019).
|
| 650 |
|
0 |
|a Automatic control.
|
| 650 |
|
0 |
|a Computer software.
|
| 710 |
2 |
|
|a ProQuest (Firm)
|
| 830 |
|
0 |
|a Princeton series in applied mathematics.
|
| 856 |
4 |
0 |
|u https://ebookcentral.proquest.com/lib/santaclara/detail.action?docID=5695063
|z Connect to this title online (unlimited simultaneous users allowed; 325 uses per year)
|t 0
|
| 907 |
|
|
|a .b32692298
|b 200401
|c 190603
|
| 998 |
|
|
|a uww
|b
|c m
|d z
|e l
|f eng
|g nju
|h 0
|
| 917 |
|
|
|a YBP DDA
|
| 919 |
|
|
|a .ulebk
|b 2017-02-14
|
| 999 |
f |
f |
|i 33d1cbca-3d21-5ab4-a2b8-36c89c3e2748
|s 30ae6281-9bf3-538e-a453-856d08754762
|t 0
|