The purpose of the example developed in this chapter is to present an interesting routing algorithm for sending messages to a mobile phone. In this example, we shall again encounter a tree structure as in the previous chapter, but this time the tree structure will be modified dynamically. We shall also encounter another example (besides the bounded re-transmission protocol in Chapter 6) where the usage of clocks will play a fundamental role. This example is taken from [1].

Informal description of the problem

A, so-called, mobile agent ℳ is supposed to travel between various sites. Fixed agents situated in the sites in question want to establish some communications with it. To simplify matters, such communications are supposed to be unidirectional: they take the practical form of messages sent from the fixed agents to ℳ.

Abstract informal specification

In an ideal abstract world, the moves of the mobile agent ℳ from one site to another are instantaneous. Likewise, the knowledge by the fixed agents of the exact position of ℳ is also supposed to be instantaneous. In that case, the fixed agents follow the mobile agent ℳ by sending messages where it currently is. Notice that such messages are (for the moment) received immediately by ℳ. This is illustrated in Fig. 12.1 where the mobile agent ℳ (represented by a black square) originally situated at site c, moves then successively to sites d, a, c, and b.

Motivation

The intent of this book is to give some insights on modeling and formal reasoning. These activities are supposed to be performed before undertaking the effective coding of a computer system, so that the system in question will be correct by construction.

In this book, we will thus learn how to build models of programs and, more generally, discrete systems. But this will be done with practice in mind. For this we shall study a large number of examples coming from various sources of computer system development: sequential programs, concurrent programs, distributed programs, electronic circuits, reactive systems, etc.

We will understand that the model of a program is quite different from the program itself. And we will learn that it is far easier to reason about the model than about the program. We will be made aware of the very important notions of abstraction and refinement; the idea being that an executable program is only obtained at the final stage of a sometimes long sequence consisting of gradually building more and more accurate models of the future program (think of the various blueprints made by an architect).

We shall make it very clear what we mean by reasoning about a model. This will be done by using some simple mathematical methods, which will be presented first by means of some examples then by reviewing classical logic (propositional and predicate calculus) and set theory. We will understand the necessity of performing proofs in a very rigorous fashion.

Informal introduction

The purpose of this chapter is to show the specification and construction of a complete computerized system. The example we are interested in is called a train system. By this, we mean a system that is practically managed by a train agent, whose role is to control the various trains crossing part of a certain track network situated under his supervision. The computerized system we want to construct is supposed to help the train agent in doing this task.

Before entering in the informal description of this system (followed by its formal construction), it might be useful to explain the reason why we think it is important to present such a case study in great detail. There are at least four reasons which are the following:

1. (i) This example presents an interesting case of quite complex data structures (the track network), whose mathematical properties have to be defined with great care: we want to show that this is possible.

2. (ii) This example also shows a very interesting case where the reliability of the final product is absolutely fundamental: several trains have to be able to cross the network safely under the complete automatic guidance of the software product we want to construct. For this reason, it will be important to study the bad incidents that could happen and which we want either to avoid completely or manage safely. In this chapter, however, we are more concerned by fault prevention than fault tolerance. We shall come back to this in the conclusion.

3. […]

In previous chapters, we used the Event-B notation and the various corresponding proof obligation rules without introducing them initially in a systematic fashion. We presented them instead in the examples when they were needed. This was sufficient for the simple examples we studied because we used part of the notation and part of the proof obligation rules only. But it might not be adequate to continue in this way when presenting more elaborate examples in subsequent chapters. The purpose of this chapter is thus to correct this. First, we present the Event-B notation as a whole, in particular the bits not used so far, and then we present all the proof obligation rules. This will be illustrated with a simple running example.

The Event-B notation

Introduction: machines and contexts

The primary concept in doing formal developments in Event-B is that of a model. A model contains the complete mathematical development of a Discrete Transition System. It is made of several components of two kinds: machines and contexts. Machines contain the dynamic parts of a model, namely variables, invariants, theorems, variants, and events, whereas contexts contain the static parts of a model, namely carrier sets, constants, axioms, and theorems. This is illustrated in Fig. 5.1. Items belonging to machines or contexts (variables, invariants, etc.) are called modeling elements.

A model can contain contexts only, or machines only, or both. In the first case, the model represents a pure mathematical structure with sets, constants, axioms, and theorems.

In this book, we are studying the correct development of distributed programs by means of various examples. So far we have done this in Chapter 4 (file transfer protocol) and in Chapter 6 (bounded retransmission protocol). In later chapters, we shall also study some distributed program developments: leader election on a ring-shaped network in Chapter 10, synchronizing processes on a tree in Chapter 11, routing algorithm in Chapter 12, leader election on a connected network in Chapter 13. We shall also study the correct development of sequential programs in Chapter 15. In this chapter, we shall study another kind of execution paradigm, namely that of concurrent programs.

Comparing distributed and concurrent programs

The distinction between sequential and distributed programs must be clear. But the one between distributed and concurrent ones might be less obvious. Here are the main differences which we consider between the two.

Distributed programs

In the case of distributed programs, the entire algorithm is performed by various agents executing some sequential programs (sometimes the same one) on different computers. But, at the same time, these agents are supposed to cooperate in order to achieve together a well-defined goal, which is the purpose of the algorithm.

This cooperation could be made easy by having a centralized agency, the role of which would be to schedule the various participating agents. But we suppose that such an agency does not exist.

In this chapter, we extend the file transfer protocol example of Chapter 4. The added constraint with regard to the previous simple example is that we suppose now that the data and acknowledgment channels situated between the two sites are unreliable. As a consequence, the effect of the execution of the bounded re-transmission protocol (for short BRP) is to only partially copy (but sometimes totally also) a sequential file from one site to another. The purpose of this example is precisely to study how we can cope with this kind of problem of dealing with fault tolerance and how we can formally reason about them. Notice that, in this chapter, we do not develop proofs as much as in the previous chapters; we only give some hints and let the reader develop the formal proof. This example has been studied in many papers among which is the one by J.F. Groote and J.C. Van de Pool [1].

Informal presentation of the bounded re-transmission protocol

Normal behavior

The sequential file to be transmitted is supposed to be transported piece by piece from one site, the sender site, to another one, the receiver site. For that purpose, the sender sends a certain data item on the so-called data channel connecting the sender to the receiver. As soon as the receiver receives this data item, it stores it in its own file and sends back an acknowledgment to the sender on the so-called acknowledgment channel connecting the receiver to the sender.

In this chapter, we shall see how to develop sequential programs. We present the approach we shall use, and then we propose a large number of examples.

Sequential programs (e.g. loops), when formally constructed, are usually developed gradually by means of a series of progressively more refined “sketches” starting with the formal specification and ending in the final program. Each such sketch is already (although often in a highly non-deterministic form) a monolithic description which resumes the final intended program in terms of a single formula. This is precisely that initial “formula”, that is gradually transformed into the final program.

We are not going to use this approach here. After all, in order to prove a large formula, a logician usually breaks it down into various pieces, on which he performs some simple manipulations before putting them together again in a final proof.

A systematic approach to sequential program development

Components of a sequential program

A sequential program is essentially made up of a number of individual assignments that are glued together by means of various constructs. Typical constructs are sequential composition (;), loop (while), and condition (if). Their role is to explicitly schedule these assignments in a proper order so that the execution of the program can achieve its intended goal.

This final chapter is entirely devoted to problems which you might try solving. They are all to be done with the Rodin Platform, which you can download from the web site “event-b.org”. We recommend beginners who are downloading the Rodin Platform for the first time to “perform” the tutorial which is included on this site before engaging in any of the problems presented in this chapter.

These problems are divided up into three categories called Exercises (Section 1), Projects (Section 2), and Mathematical developments (Section 3).

Exercises are small and easy developments, mainly corresponding to the construction of simple sequential programs. But we also find models of simple complete systems and even the development of a small electronic circuit. Exercises can be proposed in a beginner course.

Projects are more serious problems, which require more investment than exercises. They can be proposed in an advanced course.

Mathematical developments come from pure mathematics. They involve more complicated proofs than in the two previous cases; most of them are not performed automatically by the provers of the Rodin Platform. As such, they represent excellent exercises to improve our ability to perform interactive proofs.

For Exercises and Projects, we are required to write a requirements document as well as a refinement strategy before engaging in the formal development with the Rodin Platform. Most of the time, we will have to use some contexts to define the carrier sets and the constants of the problem at hand.

This title is certainly provocative. We all know that this claim corresponds to something that is impossible. No! We cannot construct faultless systems; just have a look around. If it were possible, it would have been already done a long time ago. And anyway, to begin with, what is a “fault”?

So, how can we imagine the contrary? We might think: yet another guru trying to sell us his latest universal panacea. Dear reader, be reassured, this Prologue does not contain any new bright solutions and, moreover, it is not technical; you'll have no complicated concepts to swallow. The intention is just to remind you of a few simple facts and ideas that you might use if you wish to do so.

The idea is to play the role of someone who is faced with a terrible situation (yes, the situation of computerized system development is not far from being terrible – as a measure, just consider the money thrown out of the window when systems fail). Faced with a terrible situation, we might decide to change things in a brutal way; it never works. Another approach is to gradually introduce some simple features that together will eventually result in a global improvement of the situation. The latter is the philosophy we will use here.

Introduction

The intent of this chapter is to introduce a complete example of a small system development. During this development, we will become aware of the systematic approach we are using: it consists in developing a series of more and more accurate models of the system we want to construct. This technique is called refinement. The reason for building consecutive models is that a unique one would be far too complicated to reason about. Note that each model does not represent the programming of our system using a high-level programming language, it rather formalizes what an external observer of this system could perceive of it.

Each model will be analyzed and proved, thus enabling us to establish that it is correct relative to a number of criteria. As a result, when the last model is finished, we will be able to say that this model is correct by construction. Moreover, this model will be so close to a final implementation that it will be very easy to transform it into a genuine program.

The correctness criteria alluded to above will be made completely clear and systematic by giving a number of proof obligation rules which will be applied on our models. After applying such rules, we shall have to prove formally a number of statements. To this end, we shall also give a reminder of the classical rules of inference of the sequent calculus. Such rules concern propositional logic, equality, and basic arithmetic.