{'fraction_non_alphanumeric': 0.035931893796072804, 'fraction_numerical': 0.0063017809380912, 'mean_word_length': 4.3968455147162375, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
The Unit-B Method -- Refinement Guided by Progress Concerns

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.

are gradually introduced into its design within a hierarchical development.
System properties are often categorised into two classes: safety and liveness [15]. 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 [8], liveness properties (in terms of existence and progress) amount to 45% of the overall system properties.

Motivation
In many refinement-based development methods (e.g., B [1], Event-B [2], VDM [14], Z [22]), the focus is on preserving safety properties. A common problem for such safetyoriented 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. ♦evt, i.e., infinitely often, event evt occurs) by showing that the system is deadlock free and that events other than 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 [11] 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.

An Event-B Model
The Event-B model, in Figure 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 in-  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: ( (∃ p :: st.p = waiting) ⇒ ♦(∃ p :: st.p = cs) ) (prg0) 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 request and 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 request and exit convergent (as in Figure 1). In the above expression, the notation (# x : R : T ), 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 exit decreases the first term by 2 and increases the second term by 1 while event 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 enter is not executed must be finite. It also follows that any infinite execution of the model includes an infinite number of occurrences of enter. In this case, it means that 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 Figure 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 generalized quantifier notation are taken from E.W. Dijkstra [6].
In Dijkstra's relativised quantifier notation, (∀ x : R : T ) and (∃ x : R : T ), with R the range of the quantifications and T the term, are equivalent to the more common (∀x • R ⇒ T ) and (∃x • R ∧ T ). The notation for Temporal Logic is taken from [17].  In addition to the Event-B constructs, the Unit-B model features three new ones: event coarse schedules, introduced by the keyword during; event fine schedules, introduced by the keyword upon and event indices, denoted by the square brackets next the 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., request, enter, exit) , p is an index instead of an Event-B parameter (declared with the keyword any). While a parameter is conceptually a value chosen nondeterministically, 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 request is syntatically similar to its Event-B counter part. Semantically, the difference is subtle but important. In Event-B, if request is the only enabled event, i.e. its guard is true and the guard of every of other event is false, request will be taken eventually. In Unit-B, even if request is the only enabled event, it might never occur. This is because request is not scheduled: it features neither a coarse schedule (declared with during) nor a fine schedule (declared with upon).
Events enter and exit are scheduled events: enter has both a coarse schedule and a fine schedule and exit has only a coarse schedule. In the case of exit, when its coarse schedule is continually true, i.e. some process is in its critical section and remains there, then eventually exit is taken and p exits its critical section. Event 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 enter occurs de-spite 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 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; 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 Section 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 (∀ p :: ¬st.p = cs) does not hold, there exists a process p is in its critical section, i.e., the coarse schedule of exit[p] is true. Therefore, according to its scheduling assumption, exit[p] eventually will, thus establishing (∀ p :: ¬st.p = cs) in the process thanks to the mutual exclusion invariant, inv1.
A sketched proof of (prg1) Given a process p, 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 (∀ q : p = q : ¬st.q = cs) (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 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 Section 3 and Section 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.

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 [7]. 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 [11] and a signal controller for a train station [13]. This paper is an extended version of the latter. In addition to the contributions of [13], 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.

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

Background: Computation Calculus
In this section, we give a brief introduction to computation calculus, based on [7]. 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 Section 3.
-In Section 2.1, we introduce the notion of computation predicates which can be manipulated algebraically. We use them in Section 3 to characterize the execution of Unit-B models as well as their properties. -In Section 2.2, we introduce state predicates, a special case of computation predicates which we use in Section 3 to formalize Unit-B invariants, progress and safety properties, events' guards and schedules.
-In Section 2.3, we introduce atomic computation predicates, a special case of computation predicates which we use in Section 3 to formalize the meaning of the events' actions.
Let S be the state space: a non-empty set of "states". Let C be the computation space: a set of non-empty (finite or infinite) sequences of states henceforth referred to as "computations".

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 ∈ CPred and τ ∈ C , we have, 1 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 [ s ≡ t ] 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 [5]. In particular, true (maps all computations to TRUE) and false (maps all computations to 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 ∧, ∨, ¬, ⇒, etc. The predicate algebra is extended with sequential composition as follows.
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 τ satisfies s ;t if either it is an infinite computation satisfying s, or τ can be broken into a finite prefix τ ↑ n+1 and a suffix τ ↓ n sharing state τ.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 E, F ∈ CPred have been defined for this purpose.

Definition 3 (Eternal and Finite Computations) For any predicate s,
An important property related to E (from [7]) is that for any predicate s, we have Given F, the temporal "eventually" operator (i.e., ♦) can be formulated as F; s. The "always" operator G is defined as the dual of the "eventually" operator.
Important properties of G are that it is strengthening (12), 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 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 [ G s ⇒ (Gt ⇒ G u) ] , we can reformulate it to strip the outer 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 τ, s can also be used to describe every suffix of τ. We borrow the following facts related to the notion of persistence from [7]. For all predicates s, t, and persistent u, we have G s is persistent, and (17) Consider some computation predicate r where G r holds, (17) ensures that 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; true, where p is a state predicate as defined in the subsequent.

State Predicates
A constant 1 is defined as the (left-and right-) neutral element for sequential composition.
Definition 6 (Constant 1) For any computation τ, An important property of 1 is that it is finite, i.e., In fact, 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 and 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 ∼) For any state predicate p,
For a state predicate p, the set of computations with the initial state satisfying p is captured by p ; true: the weakest such predicate. A special notation • : SPred → CPred is introduced to denote this predicate.
Definition 9 (Initially Operator •) 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 ∧ and • for ; and vice versa. Given any predicate s and any state predicate p, we have

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 X ∈ CPred is defined for this purpose.
Definition 10 (Atomic Actions) For any computation τ and predicate a, Given the above definition, the "next" operator can be expressed as X ; s for arbitrary computation s. An important property for X is that it is finite, i.e.,

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 Section 3.1, we briefly review the syntax of Unit-B models (which has been informally introduced earlier in Section 1.1.2). -In Section 3.2, we describe the semantics of a Unit-B model M. We characterize the set of executions of M by a computation predicate ex.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 Section 3.3, we provide proof rules for progress properties and prove their soundness. -In Section 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 [11].

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: 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 (:| or :∈). An event e with indices i stands for multiple events. Each corresponds to several nonindexed events e.i, one for each possible value of the indices i. Here g, c, f are state predicates. An event 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 e is carried out infinitely often. An event without any scheduling assumption will have its coarse schedule c equal to false. An event having only the coarse schedule c will have the fine schedule to be 1. Vice versa, an event having only the fine schedule f will have the coarse schedule to be 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.

Semantics
In the following, we use computation calculus to give the formal semantics of Unit-B models. Let 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, hence allows us to relate the prestate and the post-state using the state predicate s.i.x.v applied to the post-state (as indicated by X ; ). Given that an event e.i can only be carried out when it is enabled, we formulate the effect of each event execution as follows: The semantics of M is given by a computation predicate ex.M which is a conjunction of a "safety part" saf .M and a "liveness part" live.M (both to be defined later), i.e., (32) We use M ⊢ s to denote that M |= s is provable.
Properties of Unit-B models are captured by two types of properties: safety and progress (liveness).

Safety
Below, we define the general form of one step of execution of model M, i.e., step.M, and the safety constraints saf .M on its complete computations.
where 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 -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 M, in all executions of 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., G • I, either because it is an invariant or for other reasons, for any predicates s and t, we have The proof of (37) is as follows.
In the subsequent, we assume that model 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, Informally, p un q is a safety property stating that if condition p holds then it will hold continuously unless q becomes true. The formula (1 ∨ X) 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 to 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 M with invariant I and an unless property p.vun q.v. We have if for every event e and index value i with e.i ∈ M, Proof (Sketch) Condition (39) ensures that every event e.i of 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 [11, Section 2.0.1] ⊓ ⊔ 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.

Liveness
For each event of the form (29), its schedule sched.(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., G • c and the fine schedule f becomes true infinitely often, i.e., G F; •f , then eventually e.i occurs at a point where f holds, i.e., F; f ; act.(e.i). To ensure that the event 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 weak-fairness assumption for event e.i (stating that if e.i is enabled continually then eventually it will be taken) can be formulated by using c = g and f = 1. Similarly, the standard strong-fairness assumption for e.i (stating that if e.i is enabled infinitely often then eventually it will be taken) can be formulated by using c = 1 and f = g.
Instead of categorizing Unit-B events between weakly fair and strongly fair, our generalization 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 generalization facilitates this by making the transition between strong fairness to weak fairness smoother.
In Section 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 Section 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., The summary of the Unit-B modelling notation is showed in Figure 3.

Progress Properties
Progress properties are of the form p q, where is the leads-to operator. They state that every state satisfying predicate p is eventually followed by by a state satisfying q.
Definition 13 ( 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 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 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 falsifies operator which we introduce later in this section.

Definition 14 (tr operator) For any state predicate p,
The properties of and 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 falsifies properties. We can establish tr p by choosing an event e of the model and proving e falsifies p, i.e., if p holds continually e is eventually taken and whenever e is executed in a state where p holds it falsifies p.  F EN). where Property e.i falsifies p states that, when state predicate p holds, if it is not falsified by events other than e.i, e.i will eventually occur and falsify p.
Given the definition of falsifies , we have the following proof rule (taking into account the invariant I.v).
The 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), which is the most common one, the last condition (F EN) becomes trivial and can be omitted.  (15)), our goal becomes F; • ∼ p. Additionally, since [ ¬s ⇒ s ≡ s ] for any computation predicate s, we discharge our obligation by strengthening F ; • ∼ p to its negation, G • p.
Theorem 2 corresponds to the following proof rule.

Refinement
In this section, we develop rules for refining Unit-B models such that safety and liveness properties are preserved. Consider models M and N. Refinement, denoted by M ⊑ N is defined by: We call M the abstract model and N the concrete model. As a result of this definition, any property of M is also satisfied by N. Similarly to Event-B, refinement is considered in Unit-B on a per event basis. Each abstract event e a is refined by a concrete event e c .
We say that e c refines e a if The proof that N refines 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 e c is a new event. In this case, we prove that e c is the refinement of the special 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 e a and e c as follows. Given Dropping the outer G from (50), we start the proof from G F; •f a with assumption G • c a .
Finally, the proof of (49) is as follows. Expanding the definition of sched, we prove under the assumptions First, notice that we drop the outer G from (51), (52). and start the proof with the left-hand side of (51).
The following corollaries are direct consequences of Theorem 3, hence concerning events e a and e 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.  A special case of event refinement allows to remove event indices as illustrated by the following theorem.

Theorem 4 (Events' indices removal) Consider e a as follows
The following event e c is a refinement of e a , i.e., satisfying (EVT SAFE) and (EVT LIVE).
Proof For (EVT SAFE), we use E.j.v as the witness for the removing indices i, which leads to the proof obligation: act(e c . j) ⇒ act(e a .(E.j.v, j)) .
For (EVT LIVE), we note that in the case where i = E.j.v, the coarse schedule of e a is false, hence e a .i is unscheduled, hence (EVT LIVE) is satisfied. Therefore, sched.(e c .j) = sched(e a .(E.j.v, j)) holds.

Example: A Signal Control System
We illustrate our method by applying it to design a system controlling trains at a station [12]. We first present some informal requirements of the system.

Requirements
The network at the station contains an entry block, several platform blocks and an exiting block, as seen in Figure 4. Trains arrive on the network at the entry block, 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.
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).   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 summarize 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-infirst-out manner. 5th Ref. We refine further the controller's specification so that it can be implemented in some programming language.
Notation Well-definedness [19] 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 ∈ dom. f ∧ y ∈ dom .g and the formula above is therefore not necessarily well defined. This new formula x ∈ dom . f ∧ y ∈ dom .g ∧ f .x ≤ g.y is well-defined and is often a suitable substitute for f .x ≤ 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 P D(P) ∧ 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 ∈ dom . f ∧ y ∈ dom .g ⇒ f .x ≤ g.y -which is true if f .x or g.y is ill-defined and has the normal truth value otherwise -but we won't 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 Section 2 and Section 3. There we use this format in rewriting an expression with value preserving rules or various order preserving rules (e.g. ⇒, ≤), 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 ⊑ to relate two sequents in equational proofs with the understanding that Γ ⊢ ψ ⊑ Γ , α ⊢ φ stands for the inference above, i.e. Γ ⊢ ψ has a proof if Γ , α ⊢ φ 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 sequent number of the property. For example, inv0 1 is the 1st invariant of the initial model, while un2 1 and prg2 1 are the 1st unless property and the 1st progress property of the 2nd refinement, respectively.

Refinement Strategy
The refinement strategy for our development is as follows.
Initial Model focuses on specifying and reasoning about the main progress requirement FUN 2. First refinement introduces the topology of the train station ENV 3 and the movement of the trains through the station FUN 4. Second Refinement incorporates the safety requirements of the system to prevent train collisions SAF 1.
Third Refinement adds the light signals to the model EQP 5 and the assumption that the train drivers always obey these light signals ENV 6. Fourth Refinement 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. Fifth Refinement simplifies the software controller by removing the index of the corresponding event.

Initial Model M 0 -Arriving and Departing
In this initial model M 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. We attempt to use event depart to implement prg0 1 as follows.
The proof obligation (NEG 1) is trivial. However, (C EN 1) cannot be proved because the coarse schedule of depart is false (since depart is current unscheduled). We can remedy this situation by adding a coarse schedule to 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 depart has different guard and coarse schedule. It is our intention to design 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 arrive will not affect the reasoning about progress properties (it is always unscheduled), we are going to omit its refinement in the subsequent presentation.

First Refinement M 1 -The Topology
In this refinement M 1 , we first introduce the topology of the network in terms of blocks (ENV 3). We introduce a carrier set BLK = {Entry} ∪ PLF ∪ {Exit} 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 summarized in Figure 5. We use (UN) to prove that they hold. In particular, for un1 2 and un1 3, we need to strengthen the guard of 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 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.
(Split-Off-Skip) and with (prg1 2) (see below) on first leads-to property with the new property: We implement the resulting transient property, i.e., tr loc.t ∈ PLF using a new event 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 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., loc.t ∈ PLF ∧ c?
f ?, and conditions (C EN 2) and (NEG 2) can be discharged trivially. One such design is to have c? being t ∈ st ∧ loc.t ∈ PLF and f ? being true. This gives us the following design for 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 movein.
Applying the unless rule (UN), we can verify that the new events, i.e., movein and 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.

Second Refinement M 2 -Preventing Collisions
In this refinement, M 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 moveout needs to be strengthened with the fact that the exit block is free (i.e., ¬Exit ∈ 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 moveout: The scheduling information for 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 ∧ a 1 ∧ p with c 0 ∧ c 1 ∧ 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 (a 0 ∧ a 1 ∧ p c 0 ∧ c 1 ∧ p) 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 favors 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 moveout, we apply Corollary 3 (fine schedule strengthening), which requires to prove the following progress property. The abstract event moveout has no fine schedules, it is assumed to be true. Condition (F STR) is trivial since the abstract fine schedule is true. Condition (F FLW) leads to the following property: ¬Exit ∈ ran .loc , (prg2 1) which can be strengthened to true ¬Exit ∈ ran .loc (prg2 2) We satisfy prg2 2 (which is a transient property) by applying the transient rule (TRS) using event 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. Exit ∈ ran .loc ⇒ (loc −1 ).Exit ∈ st ∧ loc.( (loc −1 ).Exit ) = Exit The proofs of conditions (C EN 3) and (NEG 3) are straightforward and will be left out.
Finally we strengthen the guard of movein and subsequently strengthen its coarse schedule. We apply Corollary 2 (coarse schedule replacing) movein. The detailed proof is omitted here.

Comparison between Coarse/Fine Schedules and Weak/Strong Fairness
Event 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 weakfairness allows for t to stay where it is forever. In other words, the weak-fairness assumption for 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 moveout event using Corollary 2 will lead to the following unprovable (C STB) condition.
The event that fails to satisfy (58) is 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 moveout event refines the abstract moveout event, future refinement of 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 ∧ f for some Event e wf is scheduled with weakly fairness, event e sf is scheduled with strongly fairness. Event e 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: sched.e wf ⇐ sched.e sch ⇐ sched.e sf .
In fact, using coarse and fine schedules, we can specify a finer-grained spectrum of scheduling assumptions (compared to fairness assumptions) with the minimum being the weakfairness assumption and the maximum being the strong-fairness assumption, as can be seen in Figure 6.

Strong Fairness
Coarse/Fine Schedules Fig. 6 The spectrum of scheduling assumptions

Third Refinement -The Actuators
In this refinement M 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, moveout and 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.
The refinement of moveout is justified by applying Theorem 3 which requires us to prove the following: loc.t ∈ PLF ∩ g sgn ∧ true ⇒ ¬ Exit ∈ ran .loc (F STR 3) (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-rule (Ensure).
Ignoring safety property un3 1, we focus on prg3 1. In order to have an event to falsify loc.t ∈ PLF \ g sgn , 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, ctrl platform, indexed with the platforms. Our first design for ctrl platform is as follows.

ctrl platform [p]
during p ∈ ran .loc ∧ p ∈ PLF \ g sgn begin g sgn := g sgn ∪ {p} end The proof that ctrl platform implements prg3 1 is as follows.
Notice that we choose the coarse schedule of 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 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: p ∈ PLF ∧ p ∈ ran .loc ∧ ¬Exit ∈ ran .loc ∧ g sgn = ∅ .
Due to feasibility condition (SCH FIS), we need to strengthen the schedules of 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 ctrl platform is finalized as: ctrl platform [p] during p ∈ ran .loc ∧ p ∈ PLF \ g sgn upon ¬Exit ∈ ran .loc ∧ g sgn = ∅ when p ∈ PLF ∧ p ∈ ran .loc ∧ ¬Exit ∈ ran .loc ∧ g sgn = ∅ then g sgn := g sgn ∪ {p} end  Table 1 summarizes the design choices behind event ctrl platform.
It is interesting to see that, in this refinement, we effectively shift the fine schedule from 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 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 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 righthand side to 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 moveout event, un3 2 is a trivial safety property.
Property prg3 3 is identical to prg2 2 in the second refinement M 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.

Reusing Progress Properties
Property prg2 2, which states that the exit block becomes free infinitely often, turns out to be a key abstraction in M 2 . In M 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 M 3 and subsequent refinements.
Earlier, we have proved that M 2 satisfies prg2 2, i.e., To ensure that M 3 refines M 2 , we prove Succeed in proving (60), together with (59), will ensure that M 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 M 0 , since the property prg0 1 is eventually implemented by depart, the dependency relation can be In the first refinement, consider the dependency for prg0 1, it is dependent on event (M 1 .)depart (which is the refinement of the abstract event (M 0 .)depart) and events moveout, movein (which are used for proving the refinement of (M 0 .)depart by (M 1 .)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 M and its dependency relation: The above relation encodes the following conditions: 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 summarizes 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 M in the previous example, we replace the coarse schedule of 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 M 2 . Since prg2 2 is implemented by depart, the dependency relation for M 2 is as follows: Since depart is unchanged in M 3 , its refinement is trivial. Therefore, we are free to make use of prg2 2 in all the proofs of liveness in M 3 . It also follows that, the dependency for M 3 is the same as that of M 2 , i.e., In fact, property prg2 2 is also reused in future refinements.

Fourth Refinement -The Controller
In this refinement M 4 , we focus on realising the software controller. At the end of the previous refinement, the controller is entirely specified by 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.
invariants : In order to maintain inv4 3, we let movein increase tl and insert the platforms in the queue as they become occupied and 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 ctrl platform is refined as follows.
p ∈ dom.qe qe.p = hd ∧ ¬Exit ∈ ran .loc qe.p = hd ∧ ¬Exit ∈ ran .loc un ¬p ∈ dom .qe (C STB 5) 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 ensurerule (Ensure)). 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 pre-determined 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 moveout does, we cannot prove that moveout falsifies qe.p− hd = M . 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 ∈ ran .loc, all the platform signals are red, hence g sgn = ∅. In order to falsify qe.p − hd = M , the following steps have to happen: 1. Event depart frees the Exit block, 2. Event ctrl platform turns the platform signal to green for some platform, 3. Event 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 depart, prg4 4 with ctrl platform, and prg4 5 with moveout, according to our informal reasoning before. The detail proofs are left out.

Refinement 5 -Removal of the Event Indices
At the end of the fourth refinement, the controller event 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 ctrl platform. The final version of ctrl platform is as follows.
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.

Summary
Our development from M 0 to M 5 is driven by both safety and progress concerns. In particular, we choose on purpose to take into account liveness requirement FUN 2 at M 0 . As a result, the need to prove and maintain progress properties justifies a number of design decisions within our development. We summarize the key features and techniques of Unit-B that have illustrated throughout our case study.
M 0 We introduce the basis of modelling using scheduled events and application of transient rule (TRS) to prove simple progress properties. M 1 We illustrate how to refine scheduled events, and applications of transitivity rule (Transitivity) and ensure rule (Ensure) to prove progress properties. M 2 We discuss the difference between coarse/fine schedules and weak/strong fairness. M 3 We illustrate how progress properties that have been proved in earlier abstract models can be reused through refinement. M 4 We compare different strategies for implementing progress properties: single step (ensure and transient rules), pre-determined number of steps (transitivity rule), arbitrary finite number of steps (induction rule). M 5 We illustrate how events can be made more concrete by removing indices.

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 [10]. 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+ [17] 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) [16]. 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 [16]. 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 [17,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 [18] 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 [20], the authors combine Event-B and TLA+ for proving liveness properties in population protocols. While refinement has been used in their development, liveness prop-erties 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 L A T E X source files at the input of the tool and allowing arbitrary interleaving of model and proof elements. We use the Z3 SMT solver [21] 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 [9] exhibits these properties since it permits the user to focus on one line of reasoning at a time.

Acknowledgment
We would like to thank the anonymous reviewers for their constructive comments which helped improve the paper significantly. The first and last authors gratefully acknowledge a Discovery Grant from NSERC (National Science and Engineering Research Council).