Using Formal Description Techniques -
Abstract

Aims

This book is for readers who are not specialists in formal methods. Its aim is to introduce formal methods using the three internationally standardised FDTs (Formal Description Techniques) Estelle, LOTOS and SDL. The book allows each FDT to be studied in its own right and in comparison with the others. It also illustrates good style in the using the FDTs and shows how the FDTs can be used in development.

The target readership includes final year undergraduate students, postgraduate students, those who work with standards for computer systems, and those who wish to find out more about formal methods.

The book has substantial introductory material on formal methods and the three standardised Formal Description Techniques (FDTs). The treatment is deliberately non-mathematical to make the book widely accessible. There is guidance on how to develop specifications and implementations using the FDTs.

The book is copiously illustrated with examples that can be used to study one FDT or to compare FDTs. The examples are mainly from data communications, but they illustrate important principles in many other application areas. Little prior knowledge of data communications is required.

The book is suitable for self-study, but would also be appropriate for a practical course on formal methods and languages. A disc containing complete specifications and major diagrams is available as a companion to the book.

Contents

Part I introduces the general context of FDTs and each FDT in particular. Chapter 1 explains why FDTs were developed, their origins and their use. Chapters 2 to 4 are tutorials on Estelle, LOTOS and SDL respectively.

Part II illustrates each FDT on a graded series of examples. Chapters 5 to 9 respectively specify the Daemon Game (a simple game of chance), an Unreliable Medium, a Sliding Window Protocol, the Abracadabra Service (typical of more complex services), and the Abracadabra Protocol (that implements the Abracadabra Service).

Part III deals with development methods and tools for Estelle, LOTOS and SDL in Chapters 10 to 12 respectively.

Part IV contains reference material including references, other sources of information, and indexes.

Contributors

The contributors are FDT specialists from many countries who have helped to develop the FDTs, including Ferenc Belina, Fabrizio Bertolotti, Tom Blumer, Vijaya Chari, Ove Færgemand, Fernando Fournon, Dieter Hogrefe, Jose Mañas, Juan Quemada, Richard Tenney, Alastair Tocher, Sebastiano Trigila and Ken Turner.

Up one level to Using Formal Description Techniques