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.