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.