Marc Frappier and Henri Habrias
Springer (FACIT), 2001.
Marc Frappier and Henri Habrias
Springer (FACIT), 2001.
ISBN 1852333537 (paper)
Buy it from Amazon.com
Buy it from Amazon.co.uk
"Developing a software system without a specification is a random process. The implementation is doomed to be modified, sometimes forever, because it never precisely matches the client's needs. The goal of a specification is to capture the client's requirements in a concise, clear, unambiguous manner to minimize the risks of failure in the development process. It is much cheaper to change a specification than to change an implementation." (from the Preface)
I normally don't even try to review books on formal methods because they mostly aren't the sort of thing I would read or use. But this one is interestingly different: it sets out to provide a comparative introduction to a whole set of 'methods' (really, languages or approaches) of specifying system behaviour, using the same case study each time. Methods covered include Z. SSADM/Z, B, OMT, Action Systems, UML with CSO, VHDL, Estelle, SDL, E-LOTOS, JSD, CASL, Coq, Petri Nets and Objects - giving representative examples of each group of methods.
What's the difference between a specification and a requirement? The quotation above gives a clue: the requirement is what somebody wants, while the specification says what the system that is supposed to 'match' those wants should actually do. This distinction introduces one of the fundamental problems in requirements engineering - showing that the requirements are met, first by the specification and then by the actual implementation itself. This book has little to say about the first part of that task: tracing back from design to specification elements to requirements; but more about the second: validation.
"By its very nature, a specification cannot be 'proved' to match the client's requirements. If such a proof existed, then it would require another description of the requirements. If such a description is available, then it is a specification."
Note that even when using natural language, the authors tend towards provable statements such as the reductio ad absurdum above.
"A specification ... has the same status as axioms of a mathematical theory. They are assumed to be right... one can prove that a specification is consistent. But this is a different issue than validation."
"Validation consists essentially in stating properties about the specification, and in proving that the specification satisfies these properties. Properties describe usage scenarios at various levels of abstraction."
The example problem in the case study isn't terribly exciting -- it's just the central bit of an Invoicing system -- but it is extremely useful for (self-)teaching purposes because it melts into the background, revealing the similarities and differences in the methods themselves.
The book is very carefully produced, tightly structured, and clearly expounded. The editors have worked hard to get the distinguished authors of the chapters to keep exactly to the structure, which could certainly be defined formally as an XML DTD if you wanted.
Readers are treated to, for instance, Prof. Kenneth Turner on LOTOS, Frappier himself on JSD, Jonathan Bowen on Z, and Pascal Poizat on SDL. The approaches taken are very diverse. There is even a chapter on UML 'with a behaviour-driven method' and the familiar diagrams, so not all the chapters are full of equations. The methods include both static (state-based) and dynamic (event-based) specification approaches -- and some, like Jane Sinclair's Action Systems, do both at once. Some, like Z and CASL, consist of sets of equations; some, like VHDL look much like programming languages; others, like UML and SDL, consist in large part of diagrams with formally defined syntax.
Students and engineers who want to find out what some of those three-letter (or even 1- or 5-letter) acronyms actually mean will do well to get a copy of this book. They will be able to get started with their chosen language by studying its chapter; and of course they will be able to follow up the technical references if they need to go further.
But for me the value of a book like this is that it gives the actual feeling of what a specification would be like in the different representations. And you never know, it might even help me in my work one of these days.
© Ian Alexander 2001