Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Formal methods : an appetizer
Nielson F., Nielson H., Springer International Publishing, New York, NY, 2019. 162 pp. Type: Book (978-3-030051-55-6)
Date Reviewed: Apr 23 2020

I’ve occasionally been intimidated into ordering an appetizer as the main course, but have rarely regretted it thanks to the presence of “gourmet” friends. This is an excellent, ultra-elegant, and rigorous book. Its 160 printed pages are to be used together with its online learning environment (described in Appendix D). It is my possible abuse of the authors’ metaphor to say that the book’s eight chapters are the previously mentioned substantive appetizers, with the online complements virtually rendering many of them as full monographs (main courses).

Program graphs are introduced in Chapter 1. Their edges are labeled with such actions as y := x*y, and nodes are places in the execution. This supports the precise, mathematical introduction of semantics as total functions from actions to their transformations of memory, also known as semantic domain. The text employs a notation that is quite austere (at first impression), but the explanations’ precision ameliorates, if not eliminates, the attentive and active reader’s difficulties. Program graphs are used throughout the book as abstractions or “models” of programs.

A very pleasant and inspiring surprise is the use of E. W. Dijkstra’s seminal guarded commands (GC) [1] as a programming language, with extensions in later chapters for recursive procedures, input/output, local variables, procedures, concurrency, and more. (The authors’ MicroC is offered in addition.) Chapter 2 can serve as a wonderful tutorial on GC. I intend to reread A discipline of programming [2] with the current book open to this chapter. One modern (my word) addition to the GC language is exception handler commands (HCs), with their try, throw, and catch keywords. It was also interesting to see the short-circuit AND (&&) at this level of abstraction, after having coded it (a long time ago) in Ada to enhance execution efficiency.

Chapter 3, “Program Verification,” “work[s] directly on program graphs” and introduces the existential and universal quantifiers (of predicate logic), which, however, quantify over functions, thus effecting (a) second-order logic. The notion of logical variables (in virtual memory) is introduced: “[P]rogram variables are handled by the (concrete) memory and logical variables by the virtual memory.” These notions allow precise expressions of a predicate’s being true in all states (tautology) or true in at least one state of memory (satisfiability). These notions are at the heart of program verification, including satisfaction modulo theory (SMT) tools. I also found this chapter’s definition of predicate transformer a very helpful supplement to [2].

Chapter 4, “Program Analysis,” also known as static analysis, is the subject of the authors’ earlier, and much bigger, book [3]. Unlike program verification, program analysis can be fully automated. The abstract properties of, for example, memory are extracted, and an analysis specification is constructed. Three desiderata (my word) are semantic correctness, semantic soundness, and computational validity. Theorem 4.31 states that the latter two imply the first. (A minor puzzlement on page 48: the word “size” of array A seems to mean its “length,” the latter term being used in, I think, the rest of the book.)

Chapter 5, “Language-Based Security,” defines the notions of confidentiality, integrity, and availability as these pertain to information flow. The chapter “show[s] how formal methods can be used to ensure confidentiality and integrity.” Example 5.3 is an excellent illustration, in the GC language, of information flows that maintain confidentiality, integrity, and isolation. It is highly gratifying for me to see the following concepts, which I encountered in my work in 1985 [4], fully formalized: reference monitor; covert channel; and security-lattices, via the mathematics of partially ordered sets.

Chapter 6, “Model Checking,” covers this method: “It can be fully automated but its efficiency is usually not as good as that of program analysis. The gain is that the precision is closer to that of program verification.” Section 6.2, “Computation Tree Logic - CTL,” treats properties of paths in transition systems and comprises both state formulas and path formulas. (The program graph of a transition system has states as nodes and transitions as edges.) Regarding formal methods in general, the book does not, in the abstract, emphasize a dichotomy between theorem-proving (syntactic) and model-checking (semantic) approaches.

Chapter 7, “Procedures,” adds the semantics of functions to the GC language. This includes declarations as commands, blocks that define scope, and actions enter and exit--all familiar from such imperative languages as C, but formalized for provability/verifiability.

Chapter 8, “Concurrency,” adds concurrent/parallel execution to the GC language and displays the GC code and program graph for Lamport’s bakery algorithm in Figures 8.1 and 8.2. This example is very instructive indeed. Further exposition includes asynchronous and, separately, synchronous communication with concurrent multiplexing and demultiplexing. The chapter ends with “Broadcast and Gather (Bonus Material),” which again involves rigor-preserving extensions of the GC language.

This outstanding book sets the highest standard for education in, and promulgation of, today’s most consequential software methodology. It has my highest recommendation.

Reviewer:  George Hacken Review #: CR146954 (2009-0209)
1) Dijkstra, E. W. Guarded commands, non-determinacy and formal derivation of programs. Communications of the ACM 18, 8(1975), 453–457.
2) Dijkstra, E. W. A discipline of programming. Prentice-Hall, Englewood Cliffs, NJ, 1976.
3) Nielson, F.; Nielson, H. R.; Hankin, C. Principles of program analysis. Springer, New York, NY, 2005.
4) Computer Security Center. Department of Defense Trusted computer system evaluation criteria, CSC-STD-001-83. Department of Defense, Fort Meade, MD, 1983, https://csrc.nist.gov/csrc/media/publications/conference-paper/1998/10/08/proceedings-of-the-21st-nissc-1998/documents/early-cs-papers/dod85.pdf.
Bookmark and Share
  Reviewer Selected
Editor Recommended
Featured Reviewer
 
 
Formal Methods (D.2.4 ... )
 
 
Semantics (D.3.1 ... )
 
 
Language Constructs and Features (D.3.3 )
 
 
Software/ Program Verification (D.2.4 )
 
Would you recommend this review?
yes
no
Other reviews under "Formal Methods": Date
On a method of multiprogramming
Feijen W., van Gasteren A., Springer-Verlag New York, Inc., New York, NY, 1999. Type: Book (9780387988702)
May 1 2000
Computer-Aided reasoning: ACL2 case studies
Kaufmann M. (ed), Manolios P. (ed), Moore J. Kluwer Academic Publishers, Norwell, MA,2000. Type: Divisible Book
Jul 2 2002
Architecting families of software systems with process algebras
Bernardo M., Ciancarini P., Donatiello L. ACM Transactions on Software Engineering and Methodology 11(4): 386-426, 2002. Type: Article
Mar 10 2003
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