The title of the book, Concise guide to formal methods: theory, fundamentals and industry applications, seems promising by evoking formality, depth, breadth, and, above all, conciseness and guidance. A closer look reveals a shallow sketch of various generalities about software engineering and formal methods. Thus, the material does not provide any substance for a meaningful review. The book consists of 19 chapters that may be grouped into four major sections: (1) software engineering overview (chapters 1 and 2, 17 and 18); (2) mathematics for software engineering (chapters 4 through 7 and 16); (3) formal methods (chapters 3 and 8 through 15); and (4) an epilogue.

The book starts with an anecdotal history of the birth of software engineering and cites the meetings wherein the term “software engineering” was coined. As a motivation, it mentions the Y2K problem en passant and provides 20-year-old data rehashing the many challenges software engineering faced in its early days. The generic software life cycle, with examples such as the waterfall model, is briefly described. This introduction is followed by a glance at software reliability, areas of applications, and a list of reliability models. The remaining two chapters inform us of technology transfer and the use of formal methods in industry and lists tools available for each of the methods introduced in section 3.

The second section, which takes up on third of the book, covers a review of set theory and logic. It includes the typical material that is found in an introductory chapter or appendices in textbooks on formal methods. A later chapter introduces some basic notions of probability and statistics.

Formal methods are introduced in section 3. The first chapter starts with general notions about specifications, their importance, their applications in the industry, and criticisms of formal methods. It mentions old examples of applications of formal methods in industry. It is not an encouraging prospect to learn that these applications are over two decades old. It also provides a short summary of each of the formal methods that are elaborated in the subsequent chapters. The structure of these chapters follows a template that consists of a general introduction to the method, a simple example, a discussion of some constructs, and applications in the industry.

A chapter is dedicated for each of Z, Vienna development method (VDM), predicate transformers, model checking, and theorem proving. Somehow, Unified Modeling Language (UML) and finite state automata are also included among the formal methods, while the B method and process calculi mentioned in the introductory chapter are not addressed here. Moreover, other well-known and important formal methods are not mentioned, for example, hybrid automata could have been discussed instead of finite state automata. The presentation of each of the methods is quickly introduced through an example to illustrate the constructs of the specification language. Types, structures, and operators of the language are briefly described. The extent of the presentation does not do any justice to any of the methods.

The book is verbose and raises a serious issue about the benefits to its intended audience. In general, the presentation is wordy and brief rather than being concise. Readers with no background in formal methods are presented with unfamiliar terminology, and even more unfamiliar constructs, whereas readers with some background are presented with sketchy examples. Review questions that close each chapter are trivial, and their cognitive difficulty would be categorized as the bottom level of Bloom’s taxonomy. Neither group would benefit from this book. The author provides a number of self-references to his books to entice the reader to “explore further” what the book fails to cover.