Aims

The aim of this chapter is to show how systems with a “persistent state” can be modelled. On completion of the chapter, the reader should be able to develop models of systems which contain persistent state components. The difference between this style and the functional modelling style used so far in this book will be highlighted by revisiting the explosives controller and the trusted gateway examples.

Introduction

Using formal modelling techniques, computing systems may be described at many different levels of abstraction. The models presented so far in the book have been set at a relatively high level of abstraction. This is reflected both in the data types used and in the way functionality is described through mathematical functions that take some data representing the system as input parameters and return a result which describes the system after the computation has been performed. In some cases, the function can be described without explicitly constructing its result (e.g. see Subsection 6.4.3).

This functional modelling style has its limitations. Few computing systems are actually implemented via pure functions. More often, they have variables that hold data which are modified by operations invoked by some outside user. These variables are persistent in the sense that they continue to hold data between operation invocations. If the purpose of a model is to document design decisions about the split between ordinary parameters to functions and persistent variables it is necessary to use operations in VDM-SL. These operations take inputs and return results, but they also have some effect (often called a side-effect) on the persistent variables.

Aims

The aim of this chapter is to show how relationships between data can be modelled as mappings. The mapping type constructor and operators in VDMSL are introduced through an example from the nuclear industry. On completing this chapter, the reader should be confident in modelling and analysing systems involving mappings.

Introduction

Computing systems frequently centre on relationships between sets of values. For example, a database might link a set of customer identifiers to detailed information. Such relationships can often be modelled as mappings from elements of one set, known as the domain, to elements of the other set, known as the range. Mappings can be thought of as tables in which one can look up the domain element and read across to see the range element to which it is related. We will say that each domain element maps to the corresponding range element. Each line of the table, being a small part of the mapping, is called a maplet. Each domain element can have only one maplet in a mapping, so there is no ambiguity about which range element it points to. For example, the following table represents a mapping from names (strings of characters) to bank balances (integers).

Aims

This final chapter concerns the use of VDM in industrial practice. We aim to equip the reader to apply VDM technology cost-effectively in industrial software development processes, and to stay abreast of the state of the art in VDM and formal modelling. We aim to introduce the contribution that formal modelling can make to the tasks that are at the core of commercial development processes. We will illustrate this with several real industrial applications of VDM. Finally, we aim to provide information on the recent extensions to VDM and VDMTools, and how to gain the most from the VDM and formal methods communities.

Introduction

Modelling in a formal language is not a panacea for every problem in system and software development but, if used thoughtfully, it can yield significant benefits. The deciding factor in using VDM technology (the combination of VDM-SL and VDMTools) has to be cost-effectiveness. The cost of developing a system model during the early stages of design should be recouped when the improved understanding of system functionality reduces the reworking required to deal with defects that are uncovered during later activities such as testing and maintenance. In this chapter we discuss a range of software development activities, some of the problems that can arise during their execution and the ways in which the use of VDM can address some of these (Sections 13.2 to 13.4). Some hints on how to start using VDM are presented (Section 13.5). We illustrate the approach by describing recent industrial applications of VDM and its extended forms (Sections 13.6 and 13.7).

Aims

In this chapter, we aim to provide an awareness of the issues involved in constructing and analysing large-scale models. We will introduce modular structuring facilities in VDM-SL as an illustration of the features required in a structuring mechanism. On completion of this chapter, the reader should be able to exploit modular structuring and the potential for re-use in large models.

Introduction

In any course on modelling, one is naturally limited in the size of model which can be developed and presented. However, in any realistic application of modelling technology, questions of scale must be addressed. How can one manage the complexity of developing and analysing a model which contains many related parts?

Before answering this question, it is worth remembering that models should be kept as simple as possible while still capturing the aspects of the system which are felt to be relevant to the analysis. Careful use of abstraction means that many systems can be usefully modelled without encountering problems of scale. However, for some applications, particularly where the product is safety-related, a formally defined language such as VDM-SL must be applied to the production of a substantial model, and so the management of the model's size and complexity becomes a significant issue.

In programming languages, the management of complexity has led to the adoption of modular structuring mechanisms for programs, and this approach has also been applied to VDM-SL. All the models presented so far have been flat in the sense that they have consisted of a series of definitions in a single document.

Aims

The aim of this chapter is to introduce the use of logic for stating the properties of data and functions in system models. The logic used in VDM-SL models is introduced via a temperature monitor example. On reaching the end of the chapter, the reader should be able to state and analyse logical expressions in VDMTools Lite.

Introduction

An important advantage of building a model of a computing system is that it allows for analysis, uncovering misunderstandings and inconsistencies at an early stage in the development process. The discovery of a possible failure of the Expert To Page function in the previous chapter was the result of just such an analysis. The ability to reason about the types and functions in a model depends on having a logic (a language of logical expressions) in which to describe the properties of the system being modelled and in which to conduct arguments about whether those properties hold or not.

This chapter introduces the language of logical expressions used in VDMSL, based on Predicate Logic. It begins by introducing the idea of a predicate, then examines the basic operators which allow logical expressions to be built up from simpler expressions. Finally, we examine the mechanisms for dealing with mis-application of operators and functions in the logic of VDM-SL.

The temperature monitor

The example running through this chapter continues the chemical plant theme. Suppose we are asked to develop the software for a temperature monitor for a reactor vessel in the plant. The monitor is connected to a temperature sensor inside the vessel from which it receives a reading (in degrees Celsius) every minute.

Aims

Recursive structures are common in many applications, notably in computer language processing. They present particular modelling challenges and so we devote a chapter to them. The aim here is to show how recursive data structures such as trees and graphs are defined and used through recursive traversal. We do not introduce new VDM language concepts at this stage, but consolidate the reader's knowledge and experience by showing how VDM copes with this important class of system. We add further abstraction lessons by considering the executability of functions.

Recursive data structures: trees

Recursion arises in many significant computing applications. In Chapter 7 we introduced recursive functions as a means of traversing collections of values, and illustrated their use on sequences. However, recursion is also central to an understanding of other data structures, including trees and graphs, that arise in many significant computing applications. This chapter explores the modelling of such recursive structures further. We begin by examining tree structures and illustrate their use by examining abstract syntax trees – an application area that underpins many applications in design and programming support environments, including VDMTools. We go on to examine more general graph structures, using an application from machine code optimisation to illustrate recursive traversal. The abstraction lesson in this chapter concerns the costs and benefits of executable models.

We begin by considering a common data structure: a tree. A tree is a collection of points (termed nodes) connected to each other by links (termed arcs).

Aims

This chapter aims to introduce the reader to the most basic kinds of data value available to the modeller and to show how values can be manipulated through operators and functions. These are introduced using a traffic light kernel control example. On completing this chapter the reader should be able to recognise and use all the basic data types of VDM-SL.

Introduction

A functional model of a system is composed of definitions of types which represent the kinds of data values under consideration and definitions of functions which describe the computations performed on the data. In order to develop a formal model, we therefore require a means of defining types and values, and ways to construct logical expressions which state the properties of values. This chapter illustrates these features in VDM-SL and introduces the basic types available in VDM-SL using an example based on traffic light control. A data type (or simply type) in VDM-SL is a collection of values called the elements or members of the type. For example, the type of natural numbers consists of infinitely many elements, from zero upwards. To make use of a type, we will need

• a symbol to represent the type, e.g. nat;

• a way of writing down the type's elements, e.g. 3, “John”;

• value operators to permit the construction of more sophisticated expressions that represent elements of the type, e.g. + to represent addition; and

• comparison operators, e.g. <, to allow expressions of elements of the type to be compared.

Aims

The aim of this chapter is to show how unordered collections of values can be modelled as sets. The set type constructor and set operators in VDMSL are introduced via an example of a safety-related system. On completion of this chapter, the reader should be confident in the use of sets and the associated operators in models of systems involving collections of values.

Introduction

This is the first of three chapters that describe ways of modelling collections of data values. The three collection types covered (sets, sequences and mappings) describe progressively more structured collections. For each collection type, we will show how collections may be expressed

A formal model of a computing system should be sufficiently abstract to model the system properties of interest, and not so concrete that a great deal of irrelevant detail has to be tackled in order to understand or analyse the model. Modelling languages such as VDM-SL contain a number of features supporting such abstraction. One of the most fundamental is the facility to model sets of values without being concerned about the order in which they are stored.

Aims

The aim of this chapter is to introduce VDMTools Lite, the development environment for VDM-SL models. This is done by providing a “hands-on” tour of the tool's functionality using the alarm example introduced in Chapter 2. This chapter should enable the reader to use VDMTools Lite for exercises in the remaining part of this book.

Introduction

Models in VDM are formal in the sense that their semantics are very precisely described. This formality makes it possible to analyse models in order to confirm or refute claims about them. Such an analysis often reveals gaps in the understanding of the system, allowing these to be resolved before an expensive commitment is made to program code. The process of analysing claims about systems modelled in this way is termed validation and is discussed in greater depth in Chapter 10.

Software tools play an important role in supporting validation. This book is accompanied by an educational version of the VDM-SL version of VDMTools, called VDMTools Lite, that provides most of the functionality of the commercial tool.

This chapter introduces VDMTools Lite as a preparation for the examples and exercises of later chapters. It takes the form of a tour through the facilities for performing syntax checking, type checking, integrity checking, testing and debugging of models, using the alarm example which was presented in Chapter 2. The reader is encouraged to use the VDMTools Lite or the full VDM-SL version of VDMTools for all the exercises in this and subsequent chapters.

VDMTools Lite exists for several operating system platforms including Windows, Linux and MacOS.

Aims

The aim of this chapter is to provide a motivation for studying the modelling of computing systems by discussing the challenges of developing correct software. On completion of this chapter, the reader should be aware of the main concepts to be presented in the book and know where to find the relevant material in the text.

Software

Software is pervasive, error-prone, expensive to develop and, as an engineering medium, extraordinarily seductive. Its seemingly infinite flexibility, increasing power and the absence of physical characteristics, such as weight, make it an ideal medium in which to express complex models which might not exist at all were it not for software. As a result, software is often developed for applications which are critical either to an enterprise's mission or to the quality of life of those with whom the system interacts.

Challenged by the variety and scale of software applications, the participants in the 1968 NATO Conference on Software Engineering foresaw a discipline of software development with a sound scientific basis [Naur&69]. Over the last 40 years, there is little doubt that enormous advances have been made in our ability to control software development. However, software projects continue to suffer from serious difficulties which can lead to the delivery of faulty goods that are over budget and behind schedule.

The rapid increase in processor power has naturally led to increasing demands being made on software and its developers. Software is almost always developed as part of a larger system involving computing hardware, special systems such as sensors and actuators, human-computer interfaces and human beings.

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.

Software engineers produce many descriptions: those of the environment or domain in which a desired computing system software is to exist; descriptions of the requirements put on the software; and descriptions of the software design that implements the requirements. Thus the descriptions span the spectrum from application domain, via requirements and software architecture, program organisation and lower level designs, to executable code. While its concerns may be general, software engineering is unique among engineering disciplines in that its primary products are descriptions that must eventually satisfy the laws of mathematical logic and metamathematics.

Other engineering disciplines have to handle a quantum leap into physical reality – the stuff of natural science. In software engineering there is a different quantum leap: that from description to execution. Software engineering is thus about structuring and relating descriptions.

Abstraction and modelling taken together are the keys to mastering the complexity of environments and systems. Formal specification is employed to express abstractions and to ensure affinity to real domains. Such specifications open up ways to establish the proper relation between domain and requirements models as well as potentially verifying the links between software architecture, requirements models and the stages of design. This increases the chance of achieving a proper fit to the environment, to user expectations and of the correctness of implementation.