Flemming Nielson and Hanne Riis Nielson: Formal Methods: an appetizer
Springer, 2019, 160 pages, ISBN 978-3-030-05155-6
https://link.springer.com/book/10.1007/978-3-030-05156-3
Summary
Teaching and convincing practitioners to adopt formal methods in system engineering is admittedly still a challenge. This book aims at generating “appetite” in undergraduate students by introducing some classical formal methods trying to rely on intuition, simple examples, and a “metaformalism” rooted in graph theory which is better known than more sophisticated mathematics at the undergraduate level. The selected areas of application of formal methods are language semantics and program verification. The exposition is generally clear although the adopted notation is sometimes mathematically heavy.
This review is written by Dino Mandrioli for FME’s Book Review Committee (BRC). The aim of the BRC is to provide to the formal methods community, and to the scientific community in general, high-quality reviews of books on topics of interest to the community.
Formal Methods: an appetizer
by
Flemming Nielson and Hanne Riis Nielson.
Review
The book’s goal is to introduce and to attract students to formal methods even at an undergraduate level; in my experience an ambitious and challenging goal not only towards students but—sigh—towards the majority of colleagues. To achieve their goal, the authors aim at balancing the rigorous reasoning typical of formal methods with explanations based on intuition, examples and a careful selection of the adopted formalism(s).
In the preface and prologue formal methods (FM) are motivated; then the methods selected for the book are presented, namely program verification, program analysis, language-based security, model checking, procedure and concurrency semantics. These methods are illustrated by using program graphs and a kernel programming language rooted in guarded commands as underlying formalisms—the authors motivate this choice with the argument that graph theory and related algorithms should be better manageable by undergraduate students than more sophisticated formalisms, a choice which I can agree with. The relations among the various chapters are well explained; furthermore, several appendices aim at guiding the students to move from “passive reading and studying” to “active applying the learned material”.
The selected topics appear to this reviewer an appropriate and natural choice although centered exclusively on software semantics and analysis: it would have been nice to warn the unexperienced reader that FMs’ usefulness and application can and should go far beyond the software context, at least because software is pervasive and often part of more complex systems such as process control systems, avionics, etc., where a pure software model is useless if not integrated with a model of the interacting subsystem.
Then, chapter by chapter the various topics are developed according to the organization explained in the prologue and preface. The exposition is in general clear, precise, often elegant and gradually progressing from simplicity to depth, which makes the reading a pleasant one, at least for a reader with the appropriate background.
Indeed, the reader’s background is an issue, at least on the basis of my experience teaching FMs to computer science students, both at the undergraduate and at the graduate level. The authors claim that the only needed prerequisite is some basic programming experience. This can be true about programming—with some exception which I discuss here below—but I doubt that the average undergraduate student of most universities will “digest” an appetizer based on the mathematical notation adopted in this book. In addition, the text seems to assume a strong understanding of the difference between decidable and undecidable problems: I congratulate and envy the professors whose students satisfy these prerequisites.
A technical aspect that, in my opinion, could deserve a deeper treatment at a rather low cost is nondeterminism. The authors seem to assume an already mature understanding of such a concept. In my experience, when I introduced this concept both from the point of view of automata theory and from that of programming constructs I found students totally unprepared: it is not just a matter of defining nondeterministic abstract machines vs. deterministic ones, but to explain why in some cases the use of nondeterministic models can be useful, if not necessary. In fact, the same problem occurs when the book introduces guarded commands, where the issue is considered only marginally: most likely the students have never seen a real nondeterministic programming language. I would have expected more emphasis on the difference between a nondeterministic program where two different execution sequences––named $\omega$––produce different semantic functions—expressed in terms of memory mapping and named $\sigma$—and one where different $\omega$ lead to the same $\sigma$. The choice made in the book to use CTL for property specification provides a nice opportunity to more deeply discuss the analysis of nondeterministic systems.
As a sharply alternative choice LTL could be used instead of CTL and nondeterminism could be ignored at all but I think that with a few more details and comments the issue of nondetermism could be a major strength of the book.
Concurrency is another—traditionally critical—topic for which a deeper discussion might provide students with a greater understanding. The book treats concurrency through a natural and well-developed mathematical application of the basic program graph formalism. However, the fundamental assumption that the mathematical model works properly only as long as every action—e.g., every edge of the graph—is atomic is left implicit. An atomic language construct, however, is not guaranteed to correspond to an atomic hardware operation, so atomicity and concurrency issues trickle down to the level of hardware operations. This general problem could be illustrated—at every abstraction level—by further expanding discussions such as the one of Example 8.4: e.g., what happens if the atomic action $x_1 = 0 \lor x_2 < x_1$ is split into two separate actions $x_1 = 0$ followed by $x_2 < x_1$?
I think that this book is a pleasant and thought-provoking reading for many readers interested in FMs—though perhaps ones whose background in mathematics and theoretical computer science is deeper than that of most undergraduate students at universities I am familiar with. Indeed, the addition of just a few pages discussing topics such as those highlighted above could result in an even more stimulating new edition of the book. Frankly, I remain rather pessimistic on the probability that FMs will gain a dramatic increase in the number of fans in a short while, but this book surely cannot be blamed for this. To conclude with a little pun: the Italian translation of appetizer is “antipasto” which, literally, does not mean “generator of appetite” but “begin of the meal”; I think that the Italian term is perhaps more appropriate for the title: a good “antipasto” for already hungry readers.