Refinement

On purpose we start with one of the simplest models of computation, that given by labeled transition systems. After introducing the reader to this simple set up we start to explore what refinement might mean, beginning with trace refinement, then adding in various notions such as refusals, so that each refinement relation we introduce is more discriminating than the last. The most discriminating of all, bisimulation, will then be introduced in Chap. 2. The material in this chapter serves as the foundation of refinement in process algebras such as CSP, CCS and LOTOS which we consider in Chap. 6.

An alternative semantic model is that provided by automata, and here we explore how refinement is defined in that setting, introducing the idea of forward and backward simulations. This causes us to consider the role of infinite behaviour in more depth. We discuss completeness results, that is whether the use of simulations is sufficient to verify a refinement. Finally, we introduce the important concept of bisimulation.

One central distinction in formal methods is between those based on state, and those based on behaviour. In most applications it is essential or at least practical to have both. State based systems need behavioural elements in order to consider aspects of interaction with an environment, for example to record which changes of state are due to the system’s ongoing execution and which are in response to an externally provided stimulus. Behaviour based systems can use state and data for abstraction, for example recording the number of free spaces as a number instead of a behaviour that encodes directly how many allocation operations will still succeed. The rich research field of “integrated formal methods” considers formalisms that have both, through extensions or integration of different formalisms. We will return in detail to these issues in Chap. 9 and on. The models we have looked at so far concentrate on behaviour, and states are fully characterised by the behaviour that will be possible from that point on. Observing only the (possible) behaviour tells us everything there is to know in a LTS. In this chapter we will look at a different class of elementary models that take the complementary view. What we will be observing is states rather than behaviours; and behaviour will be implicit, in the sense that we have to draw the conclusion that “something must have happened” if we can observe that the state has changed. We observe what “is”, not directly what “happens”.

In Chap. 1 we introduced differing notions of refinement in the LTS setting - each one based upon a different notion of observation. In Chap. 2 we focused on simulations as a means to verify trace refinements in an Automata context, and we discussed both finite trace refinement as well as trace refinement in the presence of infinite traces. In Chap. 3 we developed a basic refinement model that looked at states in the first place, and constructed a relational semantics for it. We ended with sketching how labels on transitions could be added to that and how we could apply abstraction to state spaces, in preparation for the model in the current chapter. In this chapter we will look at a semantic model that is entirely based on relations and abstract state as a model of computation. In this context programs will be finite relational compositions of operations together with a finalisation which makes explicit the observations made of that program. As in Chap. 1 and ever since refinement will be the consistency of observations. We will then explore, without fixing the exact observations to be made, how simulations can be used to verify the refinement in a way similar to that found in Chap. 2.

In going from the relational semantics of CSMATs in Chap. 3 to the abstract data types of Chap. 4 we made a number of radical changes. We labelled individual transitions with the name of an operation, much as we had been doing in LTS and automata in Chaps. 1 and 2, and removed transitivity from the transition relation as we were now able to observe individual steps. We also created a separation between local (abstract) state and global (concrete) state that extended the idea of state abstraction in Chap. 3. One aspect of CSMATs that has not been fully reflected in the relational data types yet is reflexivity of the transition relation, or “stuttering”: an unchanged state could be the outcome of a labelled transition, but not every occurrence of “nothing has changed” is worth recording explicitly as a transition. This chapter will look more closely at this – leading to the concept of “perspicuous” operations in refinement. CSMATs allowed us to remain agnostic about having potentially infinite traces in the model; uncovering perspicuous operations forces us to worry about invisible things happening infinitely often (“livelock”). Thus, divergence needs to be addressed now.

This chapter looks at these issues in process algebras. As a canonical example we look at CSP, but we also discuss CCS and LOTOS. The link to the semantics is made to Chap. 1 as well as elements of Chap. 5.

This chapter defines refinement in Z, and shows how it derives from the relational model in Chap. 4. It discusses the similarities and differences with refinement in B. The approach taken in a state-based specification language is very different in emphasis from that in a process algebra. Process algebras stress the interaction between independent components (processes), so that communication and concurrency are key. State is implicit in such a description. A different approach is taken by a state-based language which, as the name suggests, considers the specification of state as the primary focus in a description. In this chapter we illustrate the approach to state-based specification by briefly introducing the Z and B notations, and showing how we can apply our theory of refinement to them.

In this chapter we consider two further state-based notations, specifically Event-B and the ASM notation. Both have similarities to Z and B, and indeed as the name suggests Event-B grew out of the B notation. Both offer more flexibility in their approach to refinement than Z and B – by adopting models closer to those in Chap. 3. One aspect of this that we discuss in this chapter is how they support refinements, and simulations, where one event or operation can be refined by several. That is, the assumption of conformality is dropped, and we discuss this below.

In the previous parts of the book, basic refinement relations were introduced semantically and for a variety of specification languages. This chapter starts the task of relating these different refinement relations by defining corresponding processes for ADT specifications, as well as process semantics for ADT specifications, and providing theorems relating refinement relations across formalisms via such embeddings.

Chapter  9 discussed the general approach to relating process refinement and relational refinement by developing a relational framework general enough that we could embed some of the refinement relations we discussed in Chap. 1. This included a brief discussion of the simulation rules that arise in the context of failures refinement (see Sect. 9.​3.​3). In this chapter we consider failures refinement in more depth, and in particular start to discuss the role that inputs and outputs have in a relational framework and how they correspond to aspects of divergence and refusals.

Chapter 9 introduced the general approach to relating process refinement and relational refinement by developing a relational framework general enough that we could embed some of the concurrent refinement relations into it. Chapter 10 built on this by looking in depth at the relationship between failures-divergences refinement and data refinement. In this chapter we now generalise the framework defined in Chap. 10 by providing a general flexible scheme for incorporating the two main “erroneous” concurrent behaviours: deadlock and divergence, into a single relational refinement relation. This is a proper generalisation in that it subsumes previous characterisations as well as allowing combinations of these.

The purpose of this book has been to explain the foundations for refinement in a variety of semantic models, and then see how these foundations are realised in some example specification languages. This has taken us on a tour through some different ways of looking at computation.