Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Formal verification of control system software
Garoche P., PRINCETON UNIVERSITY PRESS, Princeton, NJ, 2019. 224 pp. Type: Book (978-0-691181-30-1)
Date Reviewed: May 10 2021

This outstanding work manages to deal with key topics, many of which are highly advanced, while also being encyclopedic (in a good sense) within a mere 200 pages. In spite of its advanced nature, all levels of reader will be informed or well directed by it (toward, for example, a thesis or a new path of research). Clear and concrete examples, some running throughout the book, are embedded in the text at their appropriate places. There are no assigned problems; theorems are stated but not proved. The absence of proofs here is clearly necessary.

By way of illustration of the last point, I’ll name a subset of the invoked theorems and concepts that are distinctly germane to the book in various appropriate places: Hoare triples; Dijkstra’s weakest precondition; real number semantics; floating-point semantics; soundness; (in)completeness; (guaranteed) termination; (un)decidability, including Rice’s theorem; convex optimization; denotational, operational, trace, “collecting,” and axiomatic semantics; formal verification theorem-proving (deductive method), model checking, and abstract interpretation; Tarski’s fixed point theorem; Noetherian relation; Galois connection; (inductive) invariant; interval and affine arithmetic; Euler discretization; and the Lyapunov criterion and equations. These and other terms appear logically, in the right places in the book, and serve to achieve Garoche’s purpose of explicating the synthesis of control engineering and (what in my early days was called) direct digital control.

The first chapter states that this work “[should] be readable both by a control scientist unaware of formal methods, and by a computer scientist unaware of controller design.” Chapter 3’s Figure 3.1 depicts a “current development process” wherein a differential-equation-specified control system (“plant”) is discretized and presented to computer scientists for the complement of the U- (or V-) shaped project life cycle. Garoche succeeds admirably, but very demandingly of any reader, for both the control scientist and computer scientist target audiences, and thus fills a dire need for such synthesis that many of us who are concerned with high-assurance, safety-critical cyber-physical systems have felt for a very long time.

The urgency of this need has for me been borne out in particular by my long-standing, consistent observation that even some of the best designers and project managers of high-assurance, (partially) discrete control systems retain the fervent hope that “small” errors in input yield outputs close to “plant.” But for a discrete input stream and a flipped input bit, the output can be miraculously innocuous or disastrously catastrophic. The inherent unpredictability of harmless versus catastrophic has characterized conventional software development for six or seven decades. Of course, this book goes far beyond this formal methods issue.

Part 1 (of four) elaborates on formal methods and control systems, and available verification tools, which include deductive methods (also known as theorem-proving), model checking, and abstract interpretation. A damped spring-mass system, which reappears along with very clear (pseudo)code in subsequent parts of the book, lends concreteness and clarity to the exposition.

Part 2 begins with a short but lucid introduction to convex optimization, and treats the determination of abstract-interpretation invariants. The advanced nature of the subject matter--Lyapounov functions, ..., k-inductive quadratic invariants, ..., template-based analyses--makes reading this part to any depth a research project. (This is not a criticism.)

Part 3, “System-level Analysis at Model and Code Level,” considers numerical invariants that pertain to system (specification, design) properties, followed by code-level validation of system properties.

I think it was Turing Award winner Richard Hamming who said something like, “The only real numbers are the ones that can be stored in a computer’s memory.” Part 4, on floating-point semantics, authoritatively addresses perhaps the most insidious trap that these great enablers, the digital computers, have had in store for us designers of control system software: the use of real number semantics where floating-point semantics should be. Section 9.1 is an excellent explication of floating-point semantics. I can name several sections that are worth the price of the present book, and this Part 4 is one of them.

In summary, the book is well written and well organized. Some minor points: “Real semantics” stands for “real number semantics” throughout. Occasionally, prepositions do not translate well to idiomatic English, as in “nothing is assumed on [sic, about] x and y.” Also, in Example 2.7 on abstract interpretation, the singleton set {0} seems erroneously to qualify for all three signs, that is, 0, +, -. Perhaps the relations should be < or >, and not include “or equal to.”

This excellent and very demanding book addresses the critical need for synthesis that I expressed above; it addresses everything (and much more) that one didn’t learn on previous trips around the formal verification block. I recommend it highly.

Reviewer:  George Hacken Review #: CR147261 (2109-0222)
Bookmark and Share
  Featured Reviewer  
 
Verification (D.4.5 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Verification": Date
Verification of the IBM RISC System/6000 by a dynamic biased pseudo-random test program generator
Aharon A., Dorfman B., Gofman E., Leibowitz M., Schwartzburd V., Bar-David A. IBM Systems Journal 30(4): 527-538, 1991. Type: Article
Dec 1 1993
A Specification and Verification Method for Preventing Denial of Service
Yu C., Gligor V. IEEE Transactions on Software Engineering 16(6): 581-592, 1990. Type: Article
Feb 1 1991
Using program transformations to provide safety properties for real-time systems
Tsai G., Wang S. Real-Time Systems 27(2): 191-207, 2004. Type: Article
Feb 23 2005
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy