For developers of computer-based systems, capturing and understanding the complex
functional requirements and behaviour of software components has come to
represent a considerable challenge. This book aims to equip readers with skills and
techniques which will help them to address this challenge. It does so by stressing
the value of abstract system models which can be analysed and tested before an
expensive commitment is made to a particular design strategy. The book enables
the reader to understand the role and nature of abstract models as well as gain
practical experience in their creation.
In order to permit machine-supported analysis, system models must be formulated
in a well-defined notation. In this text, we use a formally defined language
called VDM-SL (the Vienna Development Method Specification Language). The
Vienna Development Method is a collection of techniques for developing computing
systems from models expressed in the language. Since its origin in an industrial
environment, VDM has become one of the most widely used of a class of techniques
known as model-oriented formal methods. The language VDM-SL was
recently standardised by the International Organization for Standardization (ISO).
Although VDM-SL is used as a teaching medium in this text, the principles taught
apply equally well to other model-based formal methods such as B, RAISE and Z.
In this book we take a pragmatic approach to the use of formal methods.We aim
to illustrate the concepts and techniques used in VDM without overwhelming the
reader with mathematics. Unlike most teaching texts on formal methods, this book
does not treat formal refinement or formal proof. Instead it focuses on the construction
of abstract and formal models for a range of computer systems. Mastering the
construction and validation of abstract models is in our view a prerequisite for
entering the world of verification.