The Unit-B method: refinement guided by progress concerns

Abstract

We present Unit-B, a formal method inspired by Event-B and UNITY. Unit-B aims at the stepwise design of software systems, satisfying safety and liveness properties. The method features the novel notion of coarse and fine schedules, a generalisation of weak and strong fairness for specifying events’ scheduling assumptions. Based on events schedules, we propose proof rules to reason about progress properties and a refinement order preserving both liveness and safety properties. We illustrate our approach by an example to show that systems development can be driven by not only safety but also liveness requirements.

1 Introduction

Developing systems satisfying their desirable properties is a non-trivial task. Formal methods have been seen as a possible solution to the problem. Given the increasing complexity of systems, many formal methods adopt refinement techniques, where systems are developed step by step in a property-preserving manner. In this way, a system’s details are gradually introduced into its design within a hierarchical development.

System properties are often categorised into two classes: safety and liveness [16]. A safety property ensures that undesirable behaviours will never happen during system executions. A liveness property guarantees that eventually desirable behaviours will happen. Ideally, systems should be developed in such a way that they satisfy both their safety and liveness requirements. Although safety properties are often considered the more important ones, we argue that having live systems is also important. A system that is safe but not live can be useless. For example, consider an elevator system that does not move. Such an elevator system is safe (nobody gets hurt), yet worthless. According to a survey [9], liveness properties (in terms of existence and progress) amount to 45 % of the overall system properties.

1.1 Motivation

In many refinement-based development methods (e.g. B [1], Event-B [2], VDM [15], Z [22]), the focus is on preserving safety properties. A common problem for such safety-oriented methods is that when applying them to the design of a system, it is possible to make the design so safe that it becomes unusable. This would happen if we strengthened the guards of the events (in Event-B) or choose strong preconditions (in B, Z, VDM) to facilitate the proof of safety properties but in such a way that, in cases where the operations or events are needed to make the system progress, they are not enabled. Concretely, in an elevator system, this might result in a controller which eventually stops opening the door to the elevator (possibly despite there being people inside) in order to satisfy the safety property that the door not be opened between floors. It is hence our aim to design a refinement framework preserving both safety and liveness properties.

UNITY  [4] has a calculus for liveness, but does not support refinement of programs. Specifications are written in the UNITY logic (a subset of temporal logic), and implementations are programs (or transition systems). The initial specification can be refined by a stronger set of temporal properties, but once the temporal properties are implemented, further refinement of the programs is not possible.

Event-B [2] has a calculus for refinement of safety properties, but does not provide much support for liveness and fairness. Instead, Event-B provides the notion of convergence. In a system, a set of events are convergent if they cannot prevent the other events from happening. This can be used, for instance, to develop model of a sequential program, to prove that the program terminates. Convergence is proven by choosing a variant for the system, i.e. an expression whose type is well ordered (e.g. natural numbers or finite sets). Then, it must be proved that all convergent events are guaranteed to decrease the variant whenever they are executed.

In Event-B, liveness properties cannot be directly expressed and proved. One justifies the validity of a liveness property (e.g. , i.e. infinitely often, event ${\mathsf{evt}}$ occurs) by showing that the system is deadlock free and that events other than ${\mathsf{evt}}$ are convergent. However, one must show that deadlock freedom is preserved in each following refinement and that all new events are convergent. If a spontaneous event (i.e. non-convergent) is needed in a refinement (e.g. an event representing an environmental action), liveness is no longer preserved. Also, only one liveness property per system can be supported.

Our Unit-B method [12] is inspired by the treatment of liveness in UNITY and refinement in Event-B. It improves on both methods by offering a notion of refinement that preserves liveness applicable to reactive and distributed systems. It does this by the introduction of coarse and fine schedules on events and event indices.

In the subsequent, we present a small example to contrast Event-B ’s safety-based style of reasoning with Unit-B ’s liveness-driven style. We present two high-level models (one in Event-B and the other in Unit-B) of a mutual exclusion protocol. In each model, we show the important safety and liveness properties that one can prove. More specifically, we study three requirements: (1) mutual exclusion (safety), (2) minimal progress and (3) individual progress.

1.1.1 An Event-B model

The Event-B model, shown in Fig. 1, formalises a set of processes ($Pcs$) each of which is in one of three states: $idle$, $waiting$and $cs$ (i.e. in their critical section). The state of every process is recorded in the (global) variable $st$ (see invariant inv0). The safety requirement of the protocol, that of mutual exclusion, is captured by invariant inv1 and can be proved at this level of abstraction.

Fig. 1

Event-B mutual exclusion specification

In order to reason about liveness in this Event-B system, we need a variant. The variant is chosen on the basis of the exact property that we want to demonstrate. We are interested in proving continuous progress, i.e. as long as there are processes waiting to enter their critical section, some process will get to enter. In linear time temporal logic, this is formulated as:

In this property, the $p$ in $st.p = waiting$ and the $p$ in $st.p = cs$ are not necessarily the same and individual processes might wait forever. There are two ways in which an execution of the Event-B model might fail to satisfy this (weak) liveness property:

• 1. The system executes forever but, after a point where some processes are waiting, only events $\mathsf{request}$ and $\mathsf{exit}$ are taken.

• 2. The system deadlocks, i.e. terminates, in a state where some processes are still waiting.

Issue 1 can be addressed by using the following variant and by making events $\mathsf{request}$ and $\mathsf{exit}$ convergent (as in Fig. 1).

In the above expression, the notation , the counting quantifier, is used to designate the number of values of $x$ that satisfy $T$ given that they satisfy $R$. Convergent events are required to decrease this natural number variant. Event $\mathsf{exit}$ decreases the first term by 2 and increases the second term by 1 while event $\mathsf{request}$ decreases the second term and leaves the first term unchanged. The two events are therefore convergent.

This line of reasoning proves that any (possibly partial) execution of the system where $\mathsf{enter}$ is not executed must be finite. It also follows that any infinite execution of the model includes an infinite number of occurrences of $\mathsf{enter}$. In this case, it means that $\mathsf{enter}$ has to occur infinitely many times in infinite executions.

Issue 2 is addressed by ensuring that, at any time, there is at least one enabled event. This is known as a proof of deadlock freedom.

In this small system, deadlock freedom is easy to prove. However, the size of its formulation grows with the number of events of the system and it cannot, in general, be broken down into smaller proof obligations.

In addition, the (weak) liveness property (prg0) is not automatically satisfied by refinements of the system. In order to preserve it, we need to make convergent all the events introduced in successive refinements and we need to prove relative deadlock freedom at each level of abstraction, a burden that only grows more daunting as a development progresses.

As mentioned earlier, this does not prove individual progress of the processes involved in the protocol. We would like to prove the following (strong) liveness property:

i.e. every process waiting eventually enters its critical section. It is not possible to prove such individual progress using the Event-B model of Fig. 1. In order to do such a proof, we would need to include in the model a description of a scheduler. In other words, a low-level design is necessary even for a high-level liveness property. This is contrary to the idea of refinement: properties should be provable at the level of abstraction and the level of details to which they pertain. This is what Unit-B accomplishes.

Notational convention The examples in this paper rely heavily on discrete mathematics and predicate calculus. With the exception of function application, we borrow the set-theoretic and relational notation from the Event-B book [2]; function application, written $f.\,x$ with $f$ the function and $x$ the argument, as well predicate calculus and generalised quantifier notation are taken from Dijkstra [7].

In Dijkstra’s relativised quantifier notation, and , with $R$ the range of the quantifications and $T$ the term, are equivalent to the more common and . The notation for temporal logic is taken from [18].

1.1.2 A Unit-B model

Figure 2 shows a Unit-B model for the same problem as Fig. 1. The Unit-B has the same set of variables and invariants as the Event-B model from Fig. 1. Figure 2 only shows the events of the Unit-B model.

Fig. 2

Unit-B mutual exclusion specification

In addition to the Event-B constructs, the Unit-B model features three new ones: event coarse schedules, introduced by the keyword $\mathsf{during }$; event fine schedules, introduced by the keyword $\mathsf{upon }$ and event indices, denoted by the square brackets next the event names. Intuitively, if the coarse schedules of an event hold continually and its fine schedules becomes true infinitely often, then the event is executed infinitely often.

For all events (i.e. $\mathsf{request}$, $\mathsf{enter}$, $\mathsf{exit}$), $p$ is an index instead of an Event-B parameter (declared with the keyword ${\mathsf{any}}$). While a parameter is conceptually a value chosen non-deterministically, an index suggests that there exists a distinct version of the event, including a separate scheduling assumption, for every one of the index’s values. This allows us to prove individual progress for each process $p$.

Event $\mathsf{request}$ is syntactically similar to its Event-B counter part. Semantically, the difference is subtle but important. In Event-B, if $\mathsf{request}$ is the only enabled event, i.e. its guard is true and the guard of every of other event is false, $\mathsf{request}$ will be taken eventually. In Unit-B, even if $\mathsf{request}$ is the only enabled event, it might never occur. This is because $\mathsf{request}$ is not scheduled: it features neither a coarse schedule (declared with $\mathsf{during }$) nor a fine schedule (declared with $\mathsf{upon }$).

Events $\mathsf{enter}$ and $\mathsf{exit}$ are scheduled events: $\mathsf{enter}$ has both a coarse schedule and a fine schedule, and $\mathsf{exit}$ has only a coarse schedule. In the case of $\mathsf{exit}$, when its coarse schedule is continually true, i.e. some process is in its critical section and remains there; then, eventually $\mathsf{exit}$ is taken and $p$ exits its critical section. Event $\mathsf{enter}$ is eventually taken if a process $p$ is waiting continually (coarse schedule) and that infinitely often no process is in its critical section (fine schedule). The fine schedule ensures that $\mathsf{enter}$ occurs despite the other processes going in and out of their critical sections.

The notion of schedule allows us to prove that certain events are guaranteed to occur without having to reference the other events. This is in contrast to Event-B where the only way to ensure that $\mathsf{enter}$ is taken is to make sure that it is eventually the only event enabled.

The next step is to formulate the liveness requirement. In UNITY logic, on which Unit-B is based, the absence of livelock (i.e. (prg0)) is formulated as:

It reads “whenever a process is waiting it eventually follows that a process, possibly a different one, will gain access to its critical section”.

Although the absence of livelock is an interesting property, it is too weak to be useful; the goal of the processes is not to allow an arbitrary other process to carry on with its work; and it is rather the goal of the mutual exclusion protocol to let the processes go about their business unhindered, independently from each other. This means that it is more important for the purpose of each process not to be left to wait forever than any other property that has to do with the competing processes. Therefore, we choose individual progress as the central property to be proved. Its UNITY formulation is:

The free variable $p$ is implicitly universally quantified over the whole formula.

In the process of proving (prg1), we will discover that another progress property is required. This is because the only way that every process can safely have a turn in their critical section is for no process to linger in theirs forever. We formulate it as (prg2) and prove it first:

It reads “infinitely often, every process will be simultaneously out of their critical section”. In LTL, they are stated as:

The standard way of proving a liveness property in Unit-B is to use rules from UNITY logic to transform the property into something that is more easily proved using the events. The rules will be explained in more details in Sect. 3. For the sake of conciseness, we only sketch the intuition behind the proofs of this example.

A sketched proof of (prg2) As long as does not hold, there exists a process $p$ is in its critical section, i.e. the coarse schedule of $\mathsf{exit}[p]$ is true. Therefore, according to its scheduling assumption, $\mathsf{exit}[p]$ eventually will, thus establishing in the process thanks to the mutual exclusion invariant, inv1.

A sketched proof of (prg1) Given a process $p$, $\mathsf{enter}[p]$ is the only event that can establish $st.p = cs$ and it does so if $st.p = waiting$ (its coarse schedule) holds continuously and (its fine schedule) is true infinitely many times. The latter is entailed by (prg2) which we already proved. The former condition is satisfied as soon as $st.p = waiting$ (the antecedent of (prg1)) is established.

It is very important to note that the index $p$ allows us to specify the scheduling assumptions on a process-by-process basis. We can thus assert and prove that every process will eventually acquire the lock (prg1), a property otherwise known as starvation freedom. This property cannot be proved in Event-B. In Event-B, we can only prove the weaker property (prg0) that some arbitrary process will eventually acquire the lock.

Traditionally, scheduling assumptions fall into two categories: weak fairness and strong fairness. In this example, weak fairness (stating that if a process $p$ is waiting and the lock is free continually, then $p$ eventually takes the lock) is insufficient to prove that process $p$ eventually takes the lock. Normally, to prove this property, the $\mathsf{enter}[p]$ event would be scheduled with strong fairness (stating that if a process $p$ is waiting and the lock is free infinitely often, then $p$ eventually holds the lock). Using strong fairness, the coarse schedule (conditions required to hold continually) and the fine schedule (conditions required to become true infinitely often) would be wrapped in a single guard, thus intertwining the reasoning about those two aspects. By decoupling these orthogonal considerations, we can reason about process $p$ waiting separately from the lock becoming free. Moreover, during refinement, this decoupling will allow us to trade freely between the coarse and the fine schedules. The distinction between coarse and fine schedules and their relation to other scheduling assumptions are explained further in Sects. 3 and  4.4.

The combination of the progress preserving refinement calculus with the novel notions of coarse and fine schedules makes it possible in Unit-B to introduce liveness properties at any stage of a development process. Reasoning about both safety and liveness can be done at the relevant abstractions. As a consequence, not only do we use liveness requirements to rule out any design decision that would be too conservative, but we also use them to guide us to the right design decisions. As a result, liveness properties, in particular progress properties, drive the development process.

1.2 Contribution

This paper features a formal semantics for Unit-B models and their properties, alongside an example of application of Unit-B to a non- trivial control problem. The semantics is formulated in computation calculus [8]. We use it to formally prove the soundness of the rules for reasoning about temporal properties and refinement relationships in Unit-B.

In the past, Unit-B has been used to design a mutual exclusion algorithm [12] and a signal controller for a train station [14]. This paper is an extended version of the latter. In addition to the contributions of [14], we (1) strengthen the separation between the formal semantics and the proof obligations, (2) present a new rule permitting the reuse of progress properties without reproving them, (3) formulate the refinement rules so as to allow the refinement of events to be justified using only one rule, (4) elaborate the individual refinement steps of the example with the design concerns that guide it and the specific proof obligations, (5) expand the example with two refinement steps leading to the specification of a controller, and (6) illustrate the use of inductive proofs of liveness in the example.

1.3 Structure

The rest of the paper is organised as follows. In Sect. 2, we review Dijkstra’s computation calculus [8] which we used to formulate our semantics and design our proofs. We follow with a description of the Unit-B method in Sect. 3. We demonstrate the method and its refinement rules by developing a signal control system in Sect. 4. We summarise our work in Sect. 5 including discussion about related work and future work.

2 Background: computation calculus

In this section, we give a brief introduction to computation calculus, based on [8]. This will be the basis for defining the semantics of Unit-B models, defining the semantics of temporal properties (both safety and liveness) and formulating the proof of soundness of the Unit-B refinement rules in Sect. 3.

• In Sect. 2.1, we introduce the notion of computation predicates which can be manipulated algebraically. We use them in Sect. 3 to characterise the execution of Unit-B models as well as their properties.

• In Sect. 2.2, we introduce state predicates, a special case of computation predicates which we use in Sect. 3 to formalise Unit-B invariants, progress and safety properties, events’ guards and schedules.

• In Sect. 2.3, we introduce atomic computation predicates, a special case of computation predicates which we use in Sect. 3 to formalise the meaning of the events’ actions.

Let $\fancyscript{S}$ be the state space: a non-empty set of “states”. Let $\fancyscript{C}$ be the computation space: a set of non-empty (finite or infinite) sequences of states henceforth referred to as “computations”.

2.1 Computation predicates

Definition 1

(Computation predicates) The set of computation predicates $CPred$ is defined as follows:

i.e. functions from computations to Booleans.

The standard Boolean operators of the predicate calculus are lifted, i.e. extended to apply to $CPred$. For example, assuming $s, t \in CPred$ and $\tau \in \fancyscript{C}$, we have,¹

The everywhere operator quantifies universally over all computations, i.e.

Whenever there are no risks of ambiguity, we shall use $s = t$ as a shorthand for for computation predicates $s, t$.

Postulate 1

$CPred$ is a predicate algebra.

A consequence of Postulate 1 is that $CPred$ satisfies all postulates for the predicate calculus as defined in [6]. In particular, $\mathbf {true}$ (maps all computations to ${\mathrm {TRUE}}$) and $\mathbf {false}$ (maps all computations to $\mathrm {FALSE}$) are the “top” and the “bottom” elements of the complete Boolean lattice with the order specified by these postulates. The lattice operations are denoted by various Boolean operators including .

The predicate algebra is extended with sequential composition as follows.

Definition 2

(Sequential composition)

(5)

where $\#$, $\uparrow$ and $\downarrow$ denote sequence operations “length”, “take” and “drop”, respectively.

Intuitively, the sequential composition of $s$ and $t$ can be understood as a program specification that requires $s$ to be run first and then $t$ to be run as soon as $s$ terminates, if it does. More specifically, a computation $\tau$ satisfies $s\,;t$ if either it is an infinite computation satisfying $s$, or $\tau$ can be broken into a finite prefix $\tau \uparrow n\! + \!1$ and a suffix $\tau \downarrow n$ sharing state $\tau .n$ such that the prefix satisfies $s$ and the suffix satisfies $t$.

In the course of reasoning using computation calculus, we make use of the distinction between infinite (“eternal”) and finite computations. Two constants $\mathbf {E}, \mathbf {F}\in CPred$ have been defined for this purpose.

Definition 3

(Eternal and finite computations) For any predicate $s$,

An important property related to $\mathbf {E}$ (from [8]) is that for any predicate $s$, we have

Given $\mathbf {F}$, the temporal “eventually” operator (i.e. $\diamondsuit$) can be formulated as $\mathbf {F};s$. The “always” operator $\mathbf {G}\,$ is defined as the dual of the “eventually” operator.

Definition 4

(Always operator) For any predicate $s$,

Important properties of $\mathbf {G}\,$ are that it is strengthening (12), it is monotonic (13), and it distributes over conjunction (14). For any predicates $s$ and $t$, we have:

A useful technique that is frequently applied is to strip all the outer $\mathbf {G}\,$ in some proofs, as illustrated in the following example. For any predicates $s$, $t$ and $u$, we have

The proof of (15) is as follows.

According to (15), whenever we need to prove a formula of the form we can reformulate it to strip the outer $\mathbf {G}\,$’s and manipulate $s$, $t$ and $u$ on their own to simplify the proof.

Definition 5

(Persistence) For any predicate $s$,

A persistent predicate describes some repetitive mosaic. If a persistent s can be used to describe a computation $\tau$, s can also be used to describe every suffix of $\tau$. We borrow the following facts related to the notion of persistence from [8]. For all predicates $s$, $t$ and persistent $u$, we have

Consider some computation predicate $r$ where $\mathbf {G}\,r$ holds, (17) ensures that $\mathbf {G}\,r$ is persistent, and (18) (together with (12)) enables us to insert $r$ after any sub-computation in a series of sequential compositions. This is particularly useful when r is an invariant, i.e. $r = p;\mathbf {true}$, where $p$ is a state predicate as defined in the subsequent.

2.2 State predicates

A constant $1\!\!1$ is defined as the (left- and right-) neutral element for sequential composition.

Definition 6

(Constant $1\!\!1$) For any computation $\tau$,

An important property of $1\!\!1$ is that it is finite, i.e.

In fact, $1\!\!1$ is the characteristic predicate of the state space. Moreover, we choose not to distinguish between a single state and the singleton computation consisting of that state, which allows us to identify predicates of one state with the predicates that hold only for singleton computations. Let us denote the set of state predicates by $SPred$.

Definition 7

(State predicate) For any predicate $p$,

A consequence of this definition is that $SPred$ is also a complete Boolean lattice with the order , with $1\!\!1$ and $\mathbf {false}$ being the “top” and “bottom” elements. It inherits all the lattice operators that it is closed under: conjunction, disjunction and existential quantification. The other lattice operations, i.e. negation and universal quantification, are defined by restricting the corresponding operators on $CPred$ to state predicates. We only use state predicate negation in this paper.

Definition 8

(State predicate negation $\sim \!$) For any state predicate $p$,

For a state predicate $p$, the set of computations with the initial state satisfying $p$ is captured by $p\,;\mathbf {true}$: the weakest such predicate. A special notation $\bullet : SPred\rightarrow CPred$ is introduced to denote this predicate.

Definition 9

(Initially operator $\bullet$) For any state predicate $p$,

This entails the validity of the following rule, which we will use anonymously in the rest of the paper: for $p, q$ two state predicates,

Another common rule related to state predicate is the state restriction rule allowing to trade $\wedge$ and $\bullet$ for ; and vice versa. Given any predicate $s$ and any state predicate $p$, we have

2.3 Atomic actions

An important operator in LTL is the “next-time operator”. This is captured in computation calculus by the notion of atomic computations: computations of length 2. A constant $\mathbf {X}\in CPred$ is defined for this purpose.

Definition 10

(Atomic actions) For any computation $\tau$ and predicate $a$,

Given the above definition, the “next” operator can be expressed as $\mathbf {X}\,;s$ for arbitrary computation $s$. An important property for $\mathbf {X}$ is that it is finite, i.e.

(28)

3 The Unit-B method

This section presents our contribution: the Unit-B method. It is inspired by Event-B  [2] and UNITY  [4].

Similar to Event-B, Unit-B is aimed at the design of software systems by stepwise refinement, where each step is verified via the application of correctness preserving refinement rules. It differs from Event-B by its capability for reasoning about progress properties and by its refinement order which preserves liveness properties. It also differs from UNITY by unifying the notions of programs and specifications, allowing stepwise refinement of programs from abstract models.

• In Sect. 3.1, we briefly review the syntax of Unit-B models (which has been informally introduced earlier in Sect. 1.1.2).

• In Sect. 3.2, we describe the semantics of a Unit-B model $\mathsf{M}$. We characterise the set of executions of $\mathsf{M}$ by a computation predicate $ex.\mathsf{M}$ which is the conjunction of a safety and a liveness component. We provide proof rules for invariant preservation and unless properties. We also show the that the proof rules are sound with respect to the semantics.

• In Sect. 3.3, we provide proof rules for progress properties and prove their soundness.

• In Sect. 3.4, we provide refinement rules and prove their soundness with respect to the semantics.

A more extensive discussion of the soundness of the proof rules of Unit-B is presented in [12].

3.1 Syntax

Similar to Event-B, a Unit-B system is modelled by a transition system, where the state space is captured by variables $v$ and the transitions are modelled by guarded events. Furthermore, Unit-B has additional assumptions on how the events should be scheduled. Using an Event-B-similar syntax, a Unit-B event has the following form:

(29)

where $i$ are the event’s indices, $g$ is the event’s guard, $c$ is the event’s coarse schedule, $f$ is the event’s fine schedule, and $s$ is the event’s action changing state variables $v$. The action is usually made up of several assignments, either deterministic ($:=$) or non-deterministic (${:\!| \hbox { or } :\in }$). An event $\mathsf{e}$ with indices $i$ stands for multiple events. Each corresponds to several non-indexed events $\mathsf{e}.i$, one for each possible value of the indices $i$. Here, $g$, $c$, $f$ are state predicates. An event $\mathsf{e}$ is said to be enabled when its guard $g$ holds. The scheduling assumption of the event is specified by $c$ and $f$ as follows: if $c$ holds continually and $f$ becomes true infinitely often, then event $\mathsf{e}$ is carried out infinitely often. An event without any scheduling assumption will have its coarse schedule $c$ equal to $\mathbf {false}$. An event having only the coarse schedule $c$ will have the fine schedule to be $1\!\!1$. Vice versa, an event having only the fine schedule $f$ will have the coarse schedule to be $1\!\!1$.

In addition to the variables and the events, a model has an initialisation state predicate $init$ constraining the initial value of the state variables. All computations of a model start from a state satisfying the initialisation and are such that, at every step, either one of its enabled events occurs or the state is unchanged, and each computation satisfies the scheduling assumptions of all events.

3.2 Semantics

In the following, we use computation calculus to give the formal semantics of Unit-B models. Let $\mathsf{M}$ be a Unit-B model containing a set of events of the form (29) and an initialisation predicate $init$. Since the action of the event can be described by a before–after predicate $s.i.v.v'$, it corresponds to an atomic action

In the above, the quantified variable $x$ is introduced to capture the before value of $v$ and hence allows us to relate the pre-state and the post-state using the state predicate $s.i.x.v$ applied to the post-state (as indicated by ). Given that an event $\mathsf{e}.i$ can only be carried out when it is enabled, we formulate the effect of each event execution as follows:

The semantics of $\mathsf{M}$ is given by a computation predicate ${ ex}.\mathsf{M}$ which is a conjunction of a “safety part” ${ saf}.\mathsf{M}$ and a “liveness part” ${ live}.\mathsf{M}$ (both to be defined later), i.e.

Definition 11

A property $s$ is satisfied by $\mathsf{M}$, denoted $\mathsf{M}\vDash s$, if the property is implied by ${ ex}.\mathsf{M}$.

(33)

We use $\mathsf{M}\vdash s$ to denote that $\mathsf{M}\vDash s$ is provable.

Properties of Unit-B models are captured by two types of properties: safety and progress (liveness).

3.2.1 Safety

Below, we define the general form of one step of execution of model M, i.e. ${ step}.\mathsf{M}$, and the safety constraints ${ saf}.\mathsf{M}$ on its complete computations.

where $\mathsf{Skip}$ is a special unscheduled event that is a part of every model. Its guard is true and its effect is to leave all the variables of model unchanged. Since the variables of the current model may be only one of the components of the state space — the other components being the variables of the models that may refine the current one — $\mathsf{Skip}$ makes no commitment about the final value of those components; that is to say that they will be changed non-deterministically without constraints.

Safety properties of the model are captured by invariance properties (also called invariants) and by unless properties.

Invariance properties An invariant $I.v$ is a state property that holds at every reachable state of the model. If $I.v$ is an invariant of $\mathsf{M}$, in all executions of $\mathsf{M}$, $I.v$ holds forever:

In particular, we rely solely on the safety part of the model to prove invariance properties, i.e. we prove . This leads to the well-known invariance principle.

Invariance properties are important for reasoning about the correctness of the models since they give an (over-) approximation of the set of reachable states. This makes it possible to use invariance properties as additional assumptions in proofs for other properties (often as a consequence of applying (17) and (18)). For example, we can propagate a state predicate $I$ to the middle of a sequential composition $s;t$ as follows: under the assumption that $I$ holds forever, i.e. $\mathbf {G}\,\bullet I$, either because it is an invariant or for other reasons, for any predicates $s$ and $t$, we have

(37)

The proof of (37) is as follows.

In the subsequent, we assume that model $\mathsf{M}$ has an invariant $I.v$.

Unless properties The other important class of safety properties is defined by the unless operator un.

Definition 12

(un operator) For any state predicates $p$, $q$,

(38)

Informally, $p\, \mathbf{un}\, q$ is a safety property stating that if condition $p$ holds, then it will hold continuously unless $q$ becomes true. The formula is used in (38) to allow the last state where $p$ holds and the state where $q$ first holds to either be the same state or immediately follow one another.

The following theorem is used for proving that a Unit-B model satisfies an unless property.

Theorem 1

(Unless rule) Consider a model $\mathsf{M}$ with invariant $I$ and an unless property $p.v\,\mathbf{un}\,q.v$. We have

if for every event $\mathsf{e}$ and index value $i$ with $\mathsf{e}.i\in \mathsf{M}$,

Proof

(Sketch) Condition (39) ensures that every event $\mathsf{e}.i$ of $\mathsf{M}$ either maintains $p$ or establishes $q$. By induction, we can see that the only way for $p$ to become false after a state where it was true is that either $q$ becomes true or that it was already true. The full proof can be found in [12, Sect. 2.0.1]. $\square$

It follows from Theorem 1 that the following proof rule can be used to prove unless properties.

The antecedent of (UN) has the interesting peculiarity that it does not include either the fine or the coarse schedule of event e.

3.2.2 Liveness

For each event of the form (29), its schedule ${ sched}.(\mathsf{e}.i)$ is formulated as follows, where $c$ and $f$ are the event’s coarse and fine schedule, respectively:

Intuitively, (SCH) states that if the coarse schedule $c$ holds continually, i.e. $\mathbf {G}\,\bullet c$ and the fine schedule $f$ becomes true infinitely often, i.e. $\mathbf {G}\,\mathbf {F};\bullet f$; then, eventually $\mathsf{e}.i$ occurs at a point where $f$ holds, i.e. ${\mathbf {F}};f; act .(\mathsf{e}.i)$. To ensure that the event $\mathsf{e}.i$ only occurs when its guard $g.i$ holds, we require the following feasibility condition:

In absence of this condition, the (coarse or fine) schedule may be continuously in contradiction with the guard: while the scheduling constraint (SCH) states that all valid computation will include occurrences of the event, the safety constraint (35) states that, under the same conditions, the event will not happen. It follows that no traces satisfy the two constraints and the system cannot be implemented.

Our coarse and fine schedules are a generalisation of the standard weak-fairness and strong-fairness assumptions. The standard 4weak-fairness assumption for event $\mathsf{e}.i$ (stating that if $\mathsf{e}.i$ is enabled continually, then eventually it will be taken) can be formulated by using $c= g$ and $f= 1\!\!1$. Similarly, the standard strong-fairness assumption for $\mathsf{e}.i$ (stating that if $\mathsf{e}.i$ is enabled infinitely often, then eventually it will be taken) can be formulated by using $c= 1\!\!1$ and $f= g$.

Instead of categorising Unit-B events between weakly fair and strongly fair, our generalisation allows us to have a little of both in every event. Strong fairness is often a nice abstraction of scheduling magic happening under the hood, but it is necessary to refine it away in order to implement it. Our generalisation facilitates this by making the transition between strong fairness to weak fairness smoother.

In Sect. 4.4.1, we provide a methodological comparison between weak and strong fairness on one hand and coarse and fine schedules on the other hand in the context of the main example. Furthermore, in Sect. 4.4 we discuss the heuristics justifying the choice of coarse and fine schedules of events.

The liveness part of the model is the conjunction of the schedules for its events, i.e.

(40)

The summary of the Unit-B modelling notation is showed in Fig. 3.

Fig. 3

Summary of Unit-B

3.3 Progress properties

Progress properties are of the form $p \rightsquigarrow q$, where $\rightsquigarrow$ is the leads-to operator. They state that every state satisfying predicate $p$ is eventually followed by a state satisfying $q$.

Definition 13

($\rightsquigarrow$ operator) For any state predicates $p$, $q$,

In the case where $p$ and $q$ contain free variables, i.e. variables not belonging to the state space, $p \rightsquigarrow q$ is understood implicitly as

with $x$ the tuple of all the free variables appearing in either $p$ or $q$. The same principle is applied to unless, transient and falsifies properties, the last two are introduced later in this section.

A special kind of progress properties is captured by the transient operator. Transient property $\mathbf{tr}\, p$ states that whenever predicate $p$ holds, it is eventually falsified. Transient properties are especially useful for creating a bridge between leads- to properties and the events that effect them. That bridge is completed by the $\mathbf{falsifies}$ operator which we introduce later in this section.

Definition 14

(tr operator) For any state predicate $p$,

The properties of $\rightsquigarrow$ and $\mathbf{tr}$ that we will use in this paper are as follows. For any state predicates $p$, $q$ and $r$, we have:

Above, in the induction rule, $M$ is a free variable and $v$ is the variant, an expression involving some state variables. The name of the (PSP) rule stands for Progress, Safety, Progress. Except for (Split-Off-Skip), the above rules are taken from [4].

We prove progress properties by relating them to the events of the model with $\mathbf{falsifies}$ properties. We can establish $\mathbf{tr}\,p$ by choosing an event $\mathsf{e}$ of the model and proving $\mathsf{e}\,\mathbf{falsifies}\, p$, i.e. if $p$ holds continually $\mathsf{e}$ is eventually taken and whenever $\mathsf{e}$ is executed in a state where $p$ holds it falsifies $p$.

Definition 15

(falsifies operator) For any state predicate $p$ and any event as follows.:

Event $\mathsf{e}$ with (actual) index $i$ falsifies property $p$ (denoted as $\mathsf{e}.i\,\mathbf{falsifies}\,p$) if under condition $p$, $\mathsf{e}.i$ negates $p$ in one step (NEG), the coarse schedule $c$ is enabled (C_EN), and the fine schedule $f$ is eventually enabled (F_EN).

where

Property $\mathsf{e}.i\,\mathbf{falsifies}\, p$ states that, when state predicate $p$ holds, if it is not falsified by events other than $\mathsf{e}.i$, $\mathsf{e}.i$ will eventually occur and falsify $p$.

Given the definition of $\mathbf{falsifies}$, we have the following proof rule (taking into account the invariant $I.v$).

The $\mathbf{falsifies}$ properties are the main tool for linking the model and the progress properties in Unit-B. The attractiveness of such properties is that we can implement them using a single event. In the case of events without a fine schedule (i.e. $f$ is $1\!\!1$), which is the most common one, the last condition (F_EN) becomes trivial and can be omitted.

Theorem 2

(Transient rule) Consider state predicate $p$ and a model $\mathsf{M}$ contains event $\mathsf{e}$.

Given an (actual) index $i$, we have

Proof

Unfolding the definitions of $\mathbf{tr}$ and $\mathbf{falsifies}$, we prove $\mathbf {G}\,\mathbf {F};\bullet \sim \! p$ under the assumptions (NEG), (C_EN) and (F_EN). Moreover, since $\mathsf{e}$ is an event in M, we have  . Therefore, we have ${ sched}.(\mathsf{e}.i)$ as an additional assumption.

Dropping the outer $\mathbf {G}\,$ in the goal and in the assumptions (similar to (15)), our goal becomes $\mathbf {F};\bullet \sim \! p$. Additionally, since for any computation predicate $s$, we discharge our obligation by strengthening $\mathbf {F}\; ; \, \bullet \! \sim \! p$ to its negation, $\mathbf {G}\,\bullet \! p$.

$\square$

Theorem 2 corresponds to the following proof rule.

3.4 Refinement

In this section, we develop rules for refining Unit-B models such that safety and liveness properties are preserved. Consider models $\mathsf{M}$ and $\mathsf{N}$. Refinement, denoted by $\mathsf{M}\sqsubseteq \mathsf{N}$, is defined by:

We call $\mathsf{M}$ the abstract model and $\mathsf{N}$ the concrete model. As a result of this definition, any property of $\mathsf{M}$ is also satisfied by $\mathsf{N}$. Similarly to Event-B, refinement is considered in Unit-B on a per event basis. Each abstract event ${\mathsf{e}}_{\mathsf{a}}$ is refined by a concrete event ${\mathsf{e}}_{\mathsf{c}}$.

(44)

(45)

We say that ${\mathsf{e}}_{\mathsf{c}}$ refines ${\mathsf{e}}_{\mathsf{a}}$ if

The proof that $\mathsf{N}$ refines $\mathsf{M}$ (i.e. (REF)) given conditions (EVT_SAFE) and (EVT_LIVE) is left out. A special case of event refinement is when the concrete event ${\mathsf{e}}_{\mathsf{c}}$ is a new event. In this case, we prove that ${\mathsf{e}}_{\mathsf{c}}$ is the refinement of the special $\mathsf{Skip}$ event which is unscheduled and does not change any variables of the abstract model.

Condition (EVT_SAFE) leads to similar proof obligations in Event-B such as guard strengthening and simulation. We focus here on expanding the condition (EVT_LIVE).

We consider two cases for event refinement: (1) the abstract and concrete events have the same indices, and (2) the indices are removed from the concrete event.

Theorem 3

(Retaining events’ indices) Consider events ${\mathsf{e}}_{\mathsf{a}}$ and ${\mathsf{e}}_{\mathsf{c}}$ as follows.

(46)

(47)

Assume (EVT_SAFE) have been proved for ${\mathsf{e}}_{\mathsf{a}}$ and ${\mathsf{e}}_{\mathsf{c}}$, i.e.

(48)

Given

then

(49)

Proof

We first prove that the left-hand side of ${ sched}.({\mathsf{e}}_{\mathsf{a}}.i)$, i.e. $\mathbf {G}\,\bullet c_a\wedge \mathbf {G}\,\mathbf {F};\bullet f_a$ eventually leads to the left-hand side of ${ sched}.({\mathsf{e}}_{\mathsf{c}}.i)$, i.e. $\mathbf {G}\,\bullet c_c\wedge \mathbf {G}\,\mathbf {F};\bullet f_c$.

(50)

Dropping the outer $G$ from (50), we start the proof from $\mathbf {G}\,\mathbf {F};\bullet f_a$ with assumption $\mathbf {G}\,\bullet c_a$.

Finally, the proof of (49) is as follows. Expanding the definition of ${ sched}$, we prove

(51)

under the assumptions

(52)

First, notice that we drop the outer $\mathbf {G}\,$ from (51), (52). and start the proof with the left-hand side of (51).

Theorem 3 leads to the following proof rule.

(53)

The following corollaries are direct consequences of Theorem 3, hence concerning events ${\mathsf{e}}_{\mathsf{a}}$ and ${\mathsf{e}}_{\mathsf{c}}$ as in (46) and (47). They illustrate different ways of refining event scheduling information: weakening the coarse schedule, replacing the coarse schedule, strengthening the fine schedule and removing the fine schedule.

Corollary 1

(Coarse schedule weakening) Given $f_c= f_a$, we have

if

(54)

Proof

(Sketch) Given $f_c= f_a$, conditions (F_FLW) and (F_STR) of Theorem 3 are trivial. Conditions (C_FLW) and (C_STB) are direct consequences of (54).

Corollary 2

(Coarse schedule replacement) Given $f_c= f_a$, we have

if

Proof

(Sketch) Given $f_c= f_a$, conditions (F_FLW) and (F_STR) of Theorem 3 are trivial.

Corollary 3

(Fine schedule strengthening) Given $c_c= c_a$, we have

if

Proof

(Sketch) Given $c_c= c_a$, conditions (C_FLW) and (C_STB) of Theorem 3 are trivial.

Corollary 4

(Fine schedule removal) Given $c_c= c_a$ and $f_c= 1\!\!1$, we have

$$\begin{aligned} { sched}.({\mathsf{e}}_{\mathsf{c}}.i) \mathbin \Rightarrow { sched}.({\mathsf{e}}_{\mathsf{a}}.i) \end{aligned}$$

if

(55)

Proof

(Sketch) Given $c_c= c_a$, conditions (C_FLW) and (C_STB) of Theorem 3 are trivial. Given $f_c= 1\!\!1$, condition (F_FLW) is trivial and condition (F_STR) is a direct consequent of (55).

A special case of event refinement allows removing event indices as illustrated by the following theorem.

Theorem 4

(Events’ indices removal) Consider ${\mathsf{e}}_{\mathsf{a}}$ as follows

(56)

The following event ${\mathsf{e}}_{\mathsf{c}}$ is a refinement of ${\mathsf{e}}_{\mathsf{a}}$, i.e. satisfying (EVT_SAFE) and (EVT_LIVE).

(57)

Proof

For (EVT_SAFE), we use $E.j.v$ as the witness for the removing indices $i$, which leads to the proof obligation:

For (EVT_LIVE), we note that in the case where $i\ne E.j.v$, the coarse schedule of ${\mathsf{e}}_{\mathsf{a}}$ is $\mathbf {false}$, hence ${\mathsf{e}}_{\mathsf{a}}.i$ is unscheduled, hence (EVT_LIVE) is satisfied. Therefore, ${ sched}.({\mathsf{e}}_{\mathsf{c}}.j) = { sched}({\mathsf{e}}_{\mathsf{a}}.(E.j.v,~j))$ holds.

4 Example: a signal control system

We illustrate our method by applying it to design a system controlling trains at a station [13]. We first present some informal requirements of the system.

4.1 Requirements

The network at the station contains an entry block, several platform blocks and an exiting block, as seen in Fig. 4. Trains arrive on the network at the entry block and then can move into one of the platform blocks before moving to the exiting block and leaving the network. In order to control the trains at the station, signals are positioned at the end of the entry block and each platform block. The train drivers are assumed to obey the signals. The signals are supposed to change from green to red automatically when a train passes by.

Fig. 4

A signal control system

The most important properties of the system are that (1) there should be no collision between trains (SAF 1) and (2) each train in the network eventually leaves (FUN 2).

SAF 1 :

There is at most one train on each block

FUN 2 :

Each train in the network eventually leaves

ENV 3 :

The tracks are arranged according to Fig. 4

FUN 4 :

Every train enters only through the entry block, then proceed to a platform block and move on to the exit block from where they leave the station.

EQP 5 :

A light signal is positioned after the entrance block and after each of the platforms.

ENV 6 :

Train drivers obey the light signals, i.e. when the signal is green, they advance and they stop when the signal is red.

Refinement strategy Our development consists of an initial model and five refinement steps. We summarise our refinement strategy for developing the signal control system as follows.

Init. model :

We abstractly model the trains in the network, focusing on FUN 2.

1st Ref. :

We introduce the topology of the network ENV 3 and FUN 4.

2nd Ref. :

We strengthen the model of the system, focusing on SAF 1.

3rd Ref. :

We introduce the signals and derive a specification for the controller that manages these signals EQP 5 and ENV 6.

4th Ref. :

We refine the controller’s specification, in particular, scheduling the trains passing the station in a first-in-first-out manner.

5th Ref. :

We refine further the controller’s specification so that it can be implemented in some programming language.

Notation Well-definedness [20] is an important issue when dealing with partial functions. However, when trying to make formulas well-defined, some overhead often has to be introduced which can make said formulas bulky. For example, if we need to express

with $f,g$ two partial functions, the formula is only meaningful in the case where $x \in {\mathrm {dom}}.f \wedge y \in {\mathrm {dom}}.g$ and the formula above is therefore not necessarily well-defined. This new formula

is well defined and is often a suitable substitute for $f.x \le g.y$ but it is much longer and the subject matter, the ordering of $f$ and $g$, constitute only a small fraction of the formula: the attention of the reader is mostly drawn to the technicality of well-definedness.

As a shorthand, we will use a new notation defined as $\langle P \rangle \triangleq \mathcal{{D}}(P) \wedge P$. In the previous example, we can express the property as

which is false if $f.x$ or $g.y$ is ill-defined and has the expected truth value otherwise. It might be also handy to have a shorthand for $x \in {\mathrm {dom}}.f \wedge y \in {\mathrm {dom}}.g \; \Rightarrow \;f.x \le g.y$ — which is true if $f.x$ or $g.y$ is ill-defined and has the normal truth value otherwise—but we will not need it in this paper and therefore refrain from defining a shorthand for it.

Logic In Sect. 3, we conducted the proofs of soundness of the refinement rules and the inference rules of temporal properties using computation calculus. In the example, we will conduct our reasoning using these inference rules and predicate calculus without reference to computation calculus. The purpose is to use the rules as a clear interface between the semantics of Unit-B and the reasoning about Unit-B models.

Proof format The equational proof format has been used to advantage already in Sects. 2 and 3. There we use this format in rewriting an expression with value preserving rules or various order preserving rules (e.g. $\Rightarrow$, $\le$), from an initial expression to a final expression. The style of manipulations has an algebraic flavour. In this section, we use equational proof format to manipulate sequents instead of normal expressions. While an expression has a value, a sequent is provable or not. The usual way of relating two sequents is the inference rule:

When building a formal proof with them, the format becomes quickly unwieldy and unreadable. Instead, we use $\sqsubseteq$ to relate two sequents in equational proofs with the understanding that $\Gamma \vdash \psi \; \sqsubseteq \;\Gamma , \alpha \vdash \phi$ stands for the inference above, i.e. $\Gamma \vdash \psi$ has a proof if $\Gamma , \alpha \vdash \phi$ has a proof.

Sometimes, inferences rules have more than one premise. In such cases, in our calculations, either we keep the most important one as the main thread of reasoning and refer to the other ones in the hint of the step, or we list the ones we kept one above the other. The subsequent steps can apply to any one of them.

Naming convention We adopt the following convention in naming the properties appearing in the subsequent development to indicate the type of the property (e.g. invariance, unless or progress), the level of refinement and the sequence number of the property. For example, inv0_1 is the first invariant of the initial model, while un2_1 and prg2_1 are the first unless property and the first progress property of the second refinement, respectively.

Refinement strategy The refinement strategy for our development is as follows.

Init. model :

focuses on specifying and reasoning about the main progress requirement FUN 2.

1st Ref. :

introduces the topology of the train station ENV 3 and the movement of the trains through the station FUN 4.

2nd Ref. :

incorporates the safety requirements of the system to prevent train collisions SAF 1.

3rd Ref. :

adds the light signals to the model EQP 5 and the assumption that the train drivers always obey these light signals ENV 6.

4th Ref. :

realises a software controller for the signals in the station. In particular, the scheduling of the train passing through the station is performed using a queue.

5th Ref. :

simplifies the software controller by removing the index of the corresponding event.

4.2 Initial model $\mathsf{M }_\mathsf{0 }$: arriving and departing

In this initial model $\mathsf{M }_\mathsf{0 }$, we use a carrier set ${TRN}$ to denote the set of trains and a variable $st$ (short for station) to denote the set of trains currently inside the station.

Initially, $st$ is assigned the empty set $\mathord \varnothing$. At this abstract level, we have two events to model a train arriving at the station and a train leaving the station as follows:

Requirement FUN 2 can be specified as a progress property (with $t$ implicitly quantified universally over the whole property):

We attempt to use event $\mathsf{depart}$ to implement prg0_1 as follows.

with:

The proof obligation (NEG_1) is trivial. However, (C_EN_1) cannot be proved because the coarse schedule of $\mathsf{depart}$ is $\mathbf {false}$ (since $\mathsf{depart}$ is current unscheduled). We can remedy this situation by adding a coarse schedule to $\mathsf{depart}$, which becomes as follows:

The updated proof obligations are:

The proof obligations C_EN_1’ and NEG_1’ can be easily discharged.

Note that event $\mathsf{depart}$ has different guard and coarse schedule. It is our intention to design $\mathsf{depart}$ with a weak guard and a strong coarse schedule that allow us to prove system properties (e.g. invariance and progress properties). This gives more flexibility in strengthening events’ guards and weakening schedules as needed during the course of refinement.

Since event $\mathsf{arrive }$ will not affect the reasoning about progress properties (it is always unscheduled), we omit its refinement in the subsequent presentation.

4.3 First refinement MchI: the topology

In this refinement ${\mathsf{M}}_{\mathsf{1}}$, we first introduce the topology of the network in terms of blocks (ENV 3). We introduce a carrier set denoting the entry block, the platform blocks and the exit block, respectively. A new variable $loc$ is added to denote the location of trains in the network, constrained by this invariant:

To capture FUN 4, we formulate the following safety properties:

They can be summarised in Fig. 5.

Fig. 5

State transitions for trains

We use (UN) to prove that they hold. In particular, for un1_2 and un1_3, we need to strengthen the guard of $\mathsf{depart}$. Subsequently, in order to make sure that the schedule is stronger than the guard (condition (SCH_FIS)), we need to strengthen the coarse schedule accordingly. An assignment for $loc$ is added for the maintenance of inv1_1.

In order to prove the refinement of $\mathsf{depart}$, we apply Corollary 2 (coarse schedule replacing). In particular, conditions (C_FLW) and (C_STB) require us to prove the following properties:

From now on, we focus on reasoning about progress properties, e.g. prg1_1, omitting the reasoning about unless properties, e.g. un1_4. The proofs of these unless properties can be done using (UN) and will be omitted here.

In order to satisfy prg1_1, we first transform it into a transient property.

with the new property:

We implement the resulting transient property, i.e. $\mathbf{tr} ~ \langle loc.t\in PLF\rangle$ using a new event $\mathsf{moveout}$. We leave the coarse and the fine schedule as some unknown $c?$ and $f?$ and see how to derive them from resulting proof obligations.

The proof that $\mathsf{moveout}$ implements the transient property is as follows.

where

²

We design the coarse schedule $c?$ and the fine schedule $f?$ such that the goal, i.e. $\langle loc.t\in PLF\rangle \wedge c?~\rightsquigarrow ~f?$, and conditions (C_EN_2) and (NEG_2) can be discharged trivially. One such design is to have $c?$ being $t\in st\; \wedge \;loc.t\in PLF$ and $f?$ being $\text {true}$. This gives us the following design for $\mathsf{moveout}$:

The updated conditions (C_EN_2) and (NEG_2) is as follows and can be discharged easily.

The remaining progress property, i.e. prg1_2, can be implemented in a similar fashion. We first transform prg1_2 into a transient property and implement it by the following new event $\mathsf{movein}$.

Applying the unless rule (UN), we can verify that the new events, i.e. $\mathsf{movein}$ and $\mathsf{moveout}$, satisfy safety constraints, such as un1_1, un1_2, un1_3 and un1_4. It should be noted that those safety requirements guided our design of the new events along side the progress properties that they are meant to satisfy.

4.4 Second refinement $\mathsf{M }_\mathsf{2 }$: preventing collisions

In this refinement, $\mathsf{M }_\mathsf{2 }$, we incorporate the safety requirement stating that there are no collisions between trains within the network, i.e. SAF 1. This is captured by a new invariant about $loc$:

The guard of event $\mathsf{moveout}$ needs to be strengthened with the fact that the exit block is free (i.e. $\lnot Exit\in \mathrm {ran}.loc$), to maintain inv2_1. Due to the feasibility condition (SCH_FIS) for Unit-B events (requiring the schedules to be stronger than the guard), we need to strengthen the schedules accordingly. In particular, we add a fine schedule to $\mathsf{moveout}$:

The scheduling information for $\mathsf{moveout}$ states that for any train $t$, if $t$ stays in a platform for infinitely long and the exit block becomes free infinitely often, then $t$ will eventually move out of the platform.

Heuristics So far, all the scheduling information was encoded in coarse schedules. It is a general principle that coarse schedules should be used over fine schedules whenever possible. This is because, contrary to fine schedules, each coarse schedule can be manipulated in separation from each other.

For example, if during refinement we want to replace the coarse schedule $a_0 \wedge a_1 \wedge p$ with $c_0 \wedge c_1 \wedge p$, we can meet the proof obligation by proving

Since the two schedules involved can be arbitrarily complex, it is often more convenient to break down the proof obligation into the following smaller ones:

Instead of seeing the replacement of the coarse schedule as one operation, we can see it as the replacement of $a_0$ with $c_0$ and $a_1$ with $c_1$. This is especially convenient because the set of concrete schedules is rarely manipulated all at once.

In comparison, when refining fine schedules, the proof obligation () has to be dealt with as a whole. The comparison between coarse and fine schedule is similar when proving liveness properties. This is why we should keep the fine schedules as small as possible.

One situation favours fine schedules. Contentions happen when many events have to occur and the occurrence of one falsifies the schedules of the others. A mutual exclusion protocol is a good example of contention. The $enter\_critical\_section$ event of each process has to occur when the process is waiting but no other process is in its critical section. When two processes, say $p_0$ and $p_1$ are waiting, if $p_0$ first enters its critical section, it falsifies $p_1$’s schedule. If it were a coarse schedule, this means that there is no guarantee that the other process will ever be granted access to its critical section. The situation can be fixed by making part of the events’ schedule coarse and the other part fine. The fact that $p_1$ is waiting is stable and no other process will falsify this. It can therefore safely be made into the coarse schedule. The other part, the condition that no other process be in their critical region, should be made into the fine schedule. It is not stable but as long as it becomes true infinitely often, $p_1$ will be granted access to its critical section.

As a rule of thumb, most schedules should be made into coarse schedules. When liveness properties cannot be proved, coarse schedules should be selectively made into fine schedules.

(end of heuristics)

In order to prove the refinement of $\mathsf{moveout}$, we apply Corollary 3 (fine schedule strengthening), which requires to prove the following progress property. The abstract event $\mathsf{moveout}$ has no fine schedules, it is assumed to be $\text {true}$. Condition (F_STR) is trivial since the abstract fine schedule is $true$. Condition (F_FLW) leads to the following property:

which can be strengthened to

We satisfy prg2_2 (which is a transient property) by applying the transient rule (TRS) using event $\mathsf{depart}$ with the index denoting the train at the $Exit$ location, i.e. $loc^{-1}.Exit$. Intuitively, the train at the exit block will eventually depart, hence the exit block becomes free.

where

The proofs of conditions (C_EN_3) and (NEG_3) are straightforward and will be left out.

Finally, we strengthen the guard of $\mathsf{movein}$ and subsequently strengthen its coarse schedule. We apply Corollary 2 (coarse schedule replacing) $\mathsf{movein}$. The detailed proof is omitted here.

4.4.1 Comparison between coarse/fine schedules and weak/strong fairness

Event $\mathsf{moveout}$ has both a coarse and a fine schedule. The alternative, using only weak or strong fairness, would complicate the proofs and make refinement of the system more difficult.

On the one hand, weak-fairness requires for the exit block to remain free continuously in order for trains to move out. This assumption is not met by the current system: if, infinitely often, another train than $t$ located at a different platform moves on to the exit block before $t$ does, $t$’s weak-fairness allows for $t$ to stay where it is forever. In other words, the weak- fairness assumption for $\mathsf{moveout}$ will be too weak; it does not guarantee that a train inside the station will eventually exit. An attempt to prove the refinement with the weakly fair $\mathsf{moveout}$ event using Corollary 2 will lead to the following unprovable (C_STB) condition.

(58)

The event that fails to satisfy (58) is $\mathsf{moveout}$ for train other than the current $t$.

On the other hand, strong-fairness would allow a train to access the exit block if it is present on the platform intermittently. This assumption is more flexible than we need since it allows behaviours where a train hops on and off the platform infinitely often while waiting for its turn at the exit block. The price of that flexibility is to entangle properties of the exit block with properties of trains: indeed, we would need not only to prove that the train will be on its platform and that the exit block will become free but that both happen simultaneously infinitely often. More formally, while we can prove that the strongly fair $\mathsf{moveout}$ event refines the abstract $\mathsf{moveout}$ event, future refinement of $\mathsf{moveout}$ will be more difficult due to the stronger scheduling assumption. We choose to relinquish this flexibility and are therefore capable of structuring our proof better: on one hand, the train stays on its platform as long as necessary; independently, the exit block becomes free infinitely many times. This (choosing a weaker scheduling assumption) is similar to choosing a weaker guard such that safety properties are satisfied: it is minimalistic and gives more flexibility for later refinements.

The relationship between our schedules (coarse/fine) and fairness assumptions (weak/strong) can be illustrated as follows. Consider the following events with identical actions. The guard of these events are also the same as $c\wedge f$ for some predicates $c$, $f$.

Event ${\mathsf{\mathsf{e}}}_{\mathsf{wf}}$ is scheduled with weakly fairness, event ${\mathsf{\mathsf{e}}}_{\mathsf{sf}}$ is scheduled with strongly fairness. Event ${\mathsf{\mathsf{e}}}_{\mathsf{sch}}$’s scheduling is split between a coarse schedule $c$ and a fine schedule $f$. Consider the strength of their scheduling assumption, we have the following relationship:

In fact, using coarse and fine schedules, we can specify a finer-grained spectrum of scheduling assumptions (compared with fairness assumptions) with the minimum being the weak-fairness assumption and the maximum being the strong-fairness assumption, as can be seen in Fig. 6.

Fig. 6

The spectrum of scheduling assumptions

4.5 Third refinement: the actuators

In this refinement $\mathsf{M}_\mathsf{3}$, we focus on requirements EQP 5 and ENV 6 which describe the light signals in the station and state the assumption that the train drivers always obey these light signals. So far, $\mathsf{moveout}$ and $\mathsf{movein}$ which model the behaviour of individual trains and their driver, state that the trains move when it is safe to. However, the drivers often cannot judge for themselves whether it is safe to proceed because they cannot see all the dangers. This is why we adopt the convention of the light signals: wherever it may be dangerous to proceed, a light signal is located and can only be green if it is safe for the train it is addressed to advance. This allows us to change the guard and schedules of the train events to only refer to information that the drivers have access to.

We continue our development by modelling the signals associated with different blocks within the network. Variable $g\_sgn$ is introduced to denote the set of platform for which the light signal is green. We focus the rest of this section on the control of the signals regulating the departure from the platforms. In particular, invariants inv3_2 and inv3_3 state that if a platform signal is green, then the exit block is free and the other platform signals are red. Invariant inv3_4 states that the signal is green only for occupied platforms.

We refine the $\mathsf{moveout}$ event to use the platform signal as follows.

The refinement of $\mathsf{moveout}$ is justified by applying Theorem 3 which requires us to prove the following:

(F_FLW_3) follows directly from the implication rule (Implication); (F_STR_3) follows from inv3_2; (C_STB_3) requires a number of simple proofs which will be left out. To discharge (C_FLW_3), we apply the ensure (Ensure) rule.

Ignoring safety property un3_1, we focus on prg3_1. In order to have an event to falsify $\langle loc.t\in PLF\setminus g\_sgn\rangle$, we need the event to add $loc.t$ to $g\_sgn$, i.e. to turn to green the signal of the platform where $t$ is. This is clearly a task of the controller rather than a model of the trains. Therefore, we introduce a controller event, $\mathsf{ctrl\_platform}$, indexed with the platforms. Our first design for $\mathsf{ctrl\_platform}$ is as follows.

The proof that $\mathsf{ctrl\_platform}$ implements prg3_1 is as follows.

where

Notice that we choose the coarse schedule of $\mathsf{ctrl\_platform}$ so as to simplify the proof of (C_EN_4). Furthermore, we choose the assignment to $g\_sgn$ in such a way as to satisfy (NEG_4).

The next step is to prove that $\mathsf{ctrl\_platform}$ satisfies the safety properties (i.e. unless properties and invariants) of the current refinement. In order to prove inv3_2 and inv3_3, we need to strengthen the guard to:

Due to feasibility condition (SCH_FIS), we need to strengthen the schedules of $\mathsf{ctrl\_platform}$ accordingly. Since strengthening the current coarse schedule will invalidate the current proof of (C_EN_4), we introduce the following new fine schedule for ctrl_platform:

Event $\mathsf{ctrl\_platform}$ is finalised as:

Table 1 summarises the design choices behind event $\mathsf{ctrl\_platform}$.

Table 1 Proof obligations and formulas justifying the design of ctrl_platform

It is interesting to see that, in this refinement, we effectively shift the fine schedule from $\mathsf{moveout}$ (an environment event) to ctrl_platform(a controller event). The model remains abstract when it comes to specify the order in which the trains gain access to the exit block but specific enough to maintain liveness.

Event $\mathsf{ctrl\_platform}$ is a specification for the computer to control the platform signals satisfying both safety and liveness properties of the overall system. In particular, the scheduling information states that if (1) a platform is occupied and the platform signal is red infinitely long and (2) the exit block is unoccupied and the other platform signals are all red infinitely often, then the system should eventually turn this platform signal to green. The refinement of event $\mathsf{movein}$ and how the entry signal is controlled is similar and omitted for the rest of the paper.

The new fine schedule changes the earlier proof of prg3_1 in two ways. First, the fine schedule gets in the antecedent of (NEG_4), which does not invalidate the proof of (NEG_4). Second, we get an additional leads-to property to prove corresponding to (F_EN).

We start the proof of (F_EN_4) by weakening its right-hand side to $\text {true}$ (consequence of transitivity (Transitivity) and implication (Implication) rules), and we keep refining it until we can implement it simply.

We leave out the detailed proof for prg3_2 and un3_2: prg3_2 is a transient property which can be implemented by $\mathsf{moveout}$ event, un3_2 is a trivial safety property.

Property prg3_3 is identical to prg2_2 in the second refinement $\mathsf{M }_\mathsf{2 }$. However, we cannot directly reuse prg2_2 since this could lead to circular reasoning. As explained below, additional precautions are required to avoid the problem.

4.5.1 Reusing progress properties

Property prg2_2, which states that the exit block becomes free infinitely often, turns out to be a key abstraction in $\mathsf{M }_\mathsf{2 }$. In $\mathsf{M}_\mathsf{3}$ and later refinements, it will be very important that the exit block be available infinitely many times so that, even if a given train misses the first opportunity to move away from its platform, it still is certain to get a turn eventually. As a result, we would like to reuse prg2_2 in the reasoning about $\mathsf{M}_\mathsf{3}$ and subsequent refinements.

Earlier, we have proved that $\mathsf{M }_\mathsf{2 }$ satisfies prg2_2, i.e.

(59)

To ensure that $\mathsf{M}_\mathsf{3}$ refines $\mathsf{M }_\mathsf{2 }$, we prove

(60)

Succeed in proving (60), together with (59), will ensure that $\mathsf{M}_\mathsf{3}$ also satisfies prg2_2. However, we cannot directly reuse prg2_2 during the proof of (60): our reasoning would be circular.

In order to avoid circular reasoning, for each model, we keep a binary relation representing the dependency between progress properties of interest and the events that contribute to their implementation. Consider the initial model $\mathsf{M }_\mathsf{0 }$, since the property prg0_1 is eventually implemented by $\mathsf{depart}$, the dependency relation can be

In the first refinement, consider the dependency for prg0_1, it is dependent on event $({\mathsf{M}}_{\mathsf{1}}.)\mathsf{depart}$ (which is the refinement of the abstract event $(\mathsf{M }_\mathsf{0 }.)\mathsf{depart}$) and events $\mathsf{moveout}$, $\mathsf{movein}$ (which are used for proving the refinement of $(\mathsf{M }_\mathsf{0 }.)\mathsf{depart}$ by $({\mathsf{M}}_{\mathsf{1}}.)\mathsf{depart})$.

More formally, the dependency relation denotes the relationship between the scheduling assumptions of the events and the property these events implement. Consider a model $\mathsf{M}$ and its dependency relation:

The above relation encodes the following conditions:

(61)

(62)

For a given model, we only need to consider the dependency relation for the progress properties that we want subsequent refinements to reuse. By default, progress properties are not reused.

In summary, the dependency relation summarises the proofs (accumulated through refinement) of progress properties. We use it in order to avoid any circular reasoning linked to the reuse of progress properties. A progress property can be reused only after its effecting events have been refined. Naturally, during the proof of refinements of these dependent events, the progress property cannot be used. This means that if, in a refinement of $\mathsf{M}$ in the previous example, we replace the coarse schedule of $\mathsf{e}_1$, we cannot use $P_1$ in the proof of (C_FLW).

Coming back to the train station example, we are interested in reusing prg2_2 which is introduced in $\mathsf{M }_\mathsf{2 }$. Since prg2_2 is implemented by $\mathsf{depart}$, the dependency relation for $\mathsf{M }_\mathsf{2 }$ is as follows:

Since $\mathsf{depart}$ is unchanged in $\mathsf{M}_\mathsf{3}$, its refinement is trivial. Therefore, we are free to make use of prg2_2 in all the proofs of liveness in $\mathsf{M}_\mathsf{3}$. It also follows that, the dependency for $\mathsf{M}_\mathsf{3}$ is the same as that of $\mathsf{M }_\mathsf{2 }$, i.e.

In fact, property prg2_2 is also reused in future refinements.

4.6 Fourth refinement: the controller

In this refinement $\mathsf{M }_\mathsf{4 }$, we focus on realising the software controller. At the end of the previous refinement, the controller is entirely specified by $\mathsf{ctrl\_platform}$ which has a fine schedule. Although the fine schedule is a useful specification mechanism, we argue that it is not readily implementable. While it is easy to produce a correct (if not efficient) implementation for an event that has only a coarse schedule — a program that tests infinitely often (every second, every minutes or every year) the schedule and execute the event when its guard is true would be a correct implementation — it is not so straightforward for a fine schedule. Repeatedly testing a fine schedule will be incorrect in a situation where the fine schedule becomes true and false infinitely many times and that the program just happens to test infinitely many times only when it is false. This naive scheduler will fail to detect that the event has to be executed.

To make our controller more deterministic, we now proceed to refining ctrl_platform’s fine schedule away. For that purpose, we introduce three new variables ($qe$, $hd$, $tl$) to model a queue. Variable $qe$ is an injective function from platform to an interval of integers where $hd$ is the index of the first element of the queue and $tl$ is the index just after the last element of the queue. This entails that the queue is empty when $hd= tl$.

As a convention, platforms are pulled at $hd$ and inserted at $tl$. Below, $[hd, tl)$ is an integer interval that includes $hd$ but excludes $tl$ and $(qe^{-1})[~\{ hd\}~]$ is the application of the inverse of $qe$ to the set $\{ hd\}$. The latter has the particularity that, when $hd$ is not in the range of $qe$, the expression evaluates to the empty set rather than being undefined.

In order to maintain inv4_3, we let $\mathsf{movein}$ increase $tl$ and insert the platforms in the queue as they become occupied and $\mathsf{moveout}$ increase $hd$ and remove the platforms as they become free.

With the queue, we can schedule the controller deterministically: to turn green the light signal of a platform, that platform has to be the head of the queue. Event $\mathsf{ctrl\_platform}$ is refined as follows.

We apply Theorem 3 to prove the refinement of $\mathsf{ctrl\_platform}$. Omitting the trivial obligations related to (F_FLW) and (F_STR), we focus on the obligations for replacing $p\in PLF\cap \mathrm {ran}.loc$ (which is equivalent to $p\in {\mathrm {dom}}.qe$) with $\langle qe.p= hd\rangle \wedge \lnot Exit\in \mathrm {ran}.loc$ for the coarse schedule of $\mathsf{ctrl\_platform}$ (i.e. conditions (C_FLW) and (C_STB)).

So far in our development, progress properties can be separated in two different groups:

• 1. Those that are satisfied in a single step. These properties are proved by transforming them into transient properties (for example, making use of rules such as ensure (Ensure) rule). Each transient property is implement by an individual event using a combination of transient rule (TRS) and falsifies rule (FLS).

• 2. Those that are satisfied in some predetermined number of steps. These properties are proved by breaking them down into several properties that can be satisfied in a single step using transitivity (Transitivity).

Property (C_FLW_5) does not fit neither categories so far. In fact, the number of steps to satisfy (C_FLW_5) depends on the position of the platform $p$ within the queue qe. As a result, in order to prove (C_FLW_5) we apply the induction rule (Induction).

We focus on the development for prg4_2. It basically says that, eventually, either the value of $qe.p- hd$ changes or $p$ is no longer in the queue. While this is exactly what $\mathsf{moveout}$ does, we cannot prove that $\mathsf{moveout}$ falsifies $\langle qe.p- hd= M \rangle$. This is because it could take as many as three steps to do that. For example, let us assume that there is a train at the $Exit$ block, i.e. $Exit\in \mathrm {ran}.loc$, all the platform signals are red, hence $g\_sgn= \mathord \varnothing$. In order to falsify $\langle qe.p- hd= M \rangle$, the following steps have to happen:

• 1. Event $\mathsf{depart}$ frees the $Exit$ block,

• 2. Event $\mathsf{ctrl\_platform}$ turns the platform signal to green for some platform,

• 3. Event $\mathsf{moveout}$ moves to the exit block the train located at the platform for which the signal is green.

As a result, we use (Transitivity) to split prg4_2 into three different properties.

Subsequently, our intention is to implement prg4_3 with $\mathsf{depart}$, prg4_4 with $\mathsf{ctrl\_platform}$ and prg4_5 with $\mathsf{moveout}$, according to our informal reasoning before. The detail proofs are left out.

4.7 Refinement 5: removal of the event indices

At the end of the fourth refinement, the controller event $\mathsf{ctrl\_platform}$ is indexed with the platform $p$ whose signal is going to be turned green. However, since $p$ is determined as the head of the queue $qe$, we can remove the index of $\mathsf{ctrl\_platform}$. The final version of $\mathsf{ctrl\_platform}$ is as follows.

The refinement of $\mathsf{ctrl\_platform}$ can be justified trivially using Theorem 4, with $(qe^{-1}).hd$ as the witness for the removed index $p$.

The first-in-first-out policy may appear too rigid because it does not allow trains to stand still at a platform for a while when they are ahead of schedule. We chose to adhere to it because of its simplicity which is a correct choice since the ability for trains to linger is not one of the stated requirements. It would, however, make for an interesting model, one which is outside the scope of this paper.

4.8 Summary

Our development from $\mathsf{M }_\mathsf{0 }$ to $\mathsf{M }_\mathsf{5 }$ is driven by both safety and progress concerns. In particular, we choose on purpose to take into account liveness requirement FUN 2 at $\mathsf{M }_\mathsf{0 }$. As a result, the need to prove and maintain progress properties justifies a number of design decisions within our development. We summarise the key features and techniques of Unit-B that have illustrated throughout our case study.

$\mathsf{M }_\mathsf{0 }$ :

We introduce the basis of modelling using scheduled events and application of transient rule (TRS) to prove simple progress properties.

${\mathsf{M}}_{\mathsf{1}}$ :

We illustrate how to refine scheduled events, and applications of transitivity rule (Transitivity) and ensure rule (Ensure) to prove progress properties.

$\mathsf{M }_\mathsf{2 }$ :

We discuss the difference between coarse/fine schedules and weak/strong fairness.

$\mathsf{M}_\mathsf{3}$ :

We illustrate how progress properties that have been proved in earlier abstract models can be reused through refinement.

$\mathsf{M }_\mathsf{4 }$ :

We compare different strategies for implementing progress properties: single step (ensure and transient rules), predetermined number of steps (transitivity rule) and arbitrary finite number of steps (induction rule).

$\mathsf{M }_\mathsf{5 }$ :

We illustrate how events can be made more concrete by removing indices.

5 Conclusion

In this paper, we presented Unit-B, a formal method inspired by Event-B and UNITY. Our method allows systems to be developed gradually via refinement and support reasoning about both safety and liveness properties. An important feature of Unit-B is the notion of coarse and fine schedules for events. Standard weak- and strong-fairness assumptions can be expressed using these event schedules. We proposed and prove the soundness of refinement rules to manipulate the coarse and fine schedules so that liveness properties are preserved automatically (i.e. without the need to reprove them). We illustrated Unit-B by developing a signal control system.

A key observation in Unit-B is the role of event scheduling regarding liveness properties being similar to the role of guards regarding safety properties. Guards prevent events from occurring in unsafe states so that safety properties will not be violated; similarly, schedules ensure the occurrence of events in order to satisfy liveness properties.

Another key aspect of Unit-B is the role of progress properties during refinement: the obligation to prove new progress properties in the application of refinement rules motivates the introduction of new events and suggests the refinement of old events. In short, the progress considerations guide the refinement of the system.

Related work Unit-B and Event-B differ mainly in the scheduling assumptions. In Event-B, event executions are assumed to satisfy a minimal progress condition: as long as there are some enabled events, one of them will be executed non-deterministically. Given this assumption, certain liveness properties can be proved for Event-B models such as progress and persistence [11]. The minimum progress assumption is often too weak to prove the required set of liveness properties. Furthermore, the liveness properties that can be proved using minimal progress have to be reproved in later refinements to ascertain that they still hold.

TLA+ [18] is another well-known formal method based on refinement supporting reasoning about liveness properties. The execution of a TLA+ model is also captured as a formula with safety and liveness sub-formulae expressed in the Temporal Logic of Actions (TLA) [17]. Actions in TLA+ (events in Unit-B) can be scheduled with weak or strong fairness. Refinement in TLA+ is based on the WF2 and SF2 rules [17]. Rule WF2 allows a weakly fair event to be refined by another weakly fair event and Rule SF2 allows a strongly fair event to be refined by another strongly fair event. The refinement rule for Unit-B is more general than the combination of WF2 and SF2: during refinement, we can trade freely between the weakly fair component (i.e. the coarse schedule) and the strongly fair component (i.e. the fine schedule). Moreover, liveness properties in TLA+ are considered to be unimportant [18, Chapter 8]. In our opinion, developing systems satisfying liveness properties is as important as ensuring that the systems satisfy safety properties. We argue that the liveness properties should be considered from the early stages of the design. Indeed, addressing liveness properties as an after thought in the design process will often lead to complicated proofs, since the model is not designed with proofs of liveness properties in mind.

See [19] for a review of the temporal logic framework developed by Manna and Pnueli. The authors use fair transition systems for the semantics of concurrent or reactive programs and temporal logic for specifying system properties. Rules are provided for proving response properties (called progress properties in this paper) that rely on just or compassionate transitions (equivalent to the weak- and strong-fairness scheduling policies) of the system for their validity. Although the Manna–Pnueli framework does not have a progress preserving refinement calculus as in Unit-B, it does have rules for data abstraction and compositional reasoning.

The idea of combining different formal methods to reason about liveness properties is also explored by other researchers. In [21], the authors combine Event-B and TLA+ for proving liveness properties in population protocols. While refinement has been used in their development, liveness properties are not preserved: progress properties have to be reproved at each level of refinement.

Future work Currently, we only consider superposition refinement in Unit-B where variables are retained during refinement. More generally, variables can be removed and replaced by other variables during refinement (data refinement). We are working on extending Unit-B to provide rules for data refinement.

Another important technique for coping with the difficulties in developing complex systems is composition/decomposition and is already a part of methods such as Event-B and UNITY. We intend to investigate on how this technique can be added to Unit-B, in particular, the role of event scheduling during composition / decomposition.

Tool support is currently under construction under the name Literate Unit-B. The goal is to integrate seamlessly the activities of modelling, proving and documenting. We do so by making equational proofs first-class citizens in models, by taking LaTeX source files at the input of the tool and allowing arbitrary interleaving of model and proof elements. We use the Z3 SMT solver [5] to discharge the proofs obligations and to validate the proof steps.

The goal is to allow the user to formulate formal proofs in a clear manner and integrate them in the documentation of the models, letting the tool verify that every step of reasoning is sound or suggest where a lemma would be needed to justify a step. Such a tool is needed for the Unit-B method to be practical. This tool substantially reduces the burden of validity checking, therefore allowing developers to focus on the software design.

As is the case with Rodin [3], the tool for Event-B, a large percentage of proof obligations can be discharged automatically, freeing the user from the need to check many simple facts. This leaves him with the job of proving only the hardest obligations. It is useful then to be able to design and present the proof of these hard theorems using a format that is both readable by humans and amenable to formal reasoning by humans. We believe the equational format [10] exhibits these properties since it permits the user to focus on one line of reasoning at a time.