Formal method Event-B supports refinement as a means to divide a proof problem into different ones. To make the divided proofs easier to prove, we need to find an appropriate dividing strategy in refinement. At the same time, we should consider some other conditions given as proof obligations, and also how to formalize the specification. We think one of the reasons why EventB is not accessible for developers is the simultaneity of these considerations in refinement. In this paper, we propose a modeling guideline to separate the consideration of the dividing strategy from Event-B formalism. We use a treestructured diagram to design the dividing strategy in our guideline. We show a case study to confirm the feasibility of our approach.
Event-B is a well-established formal method for developing systems and proving their safety requirements. In industrial development, because specification description needs to be developed in natural language to agree with clients, we think Event-B can be useful to prove specification which has been developed in an informal way rather than to develop proved specification. However, Event-B is still unfamiliar to developers, specifically designers and architects. We think that's because Event-B is not so accessible for them. So, we should present Event-B in a more accessible way when we educate developers. Especially, we think refinement is one of the most difficult aspects to present to developers.
In Event-B refinement, we can express and prove a safety requirement on an abstract formal model of the system. Design details of the system are later gradually introduced into the formal models. During refinement, the proved safety requirement is preserved if and only if the abstract model simulates a concrete model, which is called simulation constraint in this paper. This means that refinement enables us to divide the proof on the concrete model into the proof on the abstract model and the simulation constraint. However, except for the simulation constraint, refinement doesn't provide any other guides or constraints on how to divide the proof problem by gradually refining the abstract model into concrete models. In this paper, we call a strategy to divide a proof problem Dividing Strategy. Moreover, we think modeling specification in Event-B is not so trivial. We have several choices to formalize a given specification in Event-B semantics. It means we also have to consider how to formalize the specification during refinement.
Motivation. For the reason above, we have to consider the following three things at
the same time in Event-B refinement: (
Contribution. Our contribution in this paper is to propose an Event-B modeling
guideline in which (
Structure. The rest of this paper is structured as follows. In Section 2, we briefly review the Event-B modeling method. We motivate and present our approach in Section 3. We propose a modeling guideline with DST in Section 4. We provide an example developed according to our proposed guideline in Section 5. We discuss the benefits and limitations of our approach in Section 6. Related works are discussed in Section 7. Finally we draw conclusions and suggest future work in Section 8. 2
Event-B represents a further evolution of the classical B-method [2]. Event-B has a semantics based on transition systems and simulation between such systems. Event-B models are organized according to two constructs: contexts and machines. Contexts. Contexts specify the static part of a model and may contain carrier sets, constants, axioms and theorems. Because we will not refer to contexts in this paper, we omit the details of them.
Machines. Machines specify behavioral properties of Event-B models. Machines may contain variables, invariants, theorems and events. Variables denoted by v define the state of a machine. They are constrained by invariants I(v). Theorems are properties derivable from the invariants. Possible state changes are described by events. An event e can be represented by the term
e ≘ any t where G(t ; v) then S(t ; v) end , where t denotes the event's parameters, G(t ; v) is the event's guard, and S(t ; v) is the event's action. The guard states the condition under which an event may occur, and the action describes how the state variables are updated when the event occurs. The event's action is composed of one or more assignments of the form x ≔ E(t ; v), where x is a variable in v, and E is an expression.
Refinement. Refinement provides a means to gradually introduce details of the specification into models [1]. A concrete machine can refine another abstract machine. At the moment, any behavior of the concrete machine should be simulated by a behavior of the abstract machine (simulation constraint). The simulation constraint is represented as logical proof assignments, which are called proof obligations.
Refinement can be done hierarchically, and a property proved in the abstract machine is then preserved in the concrete machines. Since the abstract machine contains fewer details than the concrete machines, the safety requirement in the abstract machine is usually easier to prove. Refinement enables us to divide a proof problem into different ones. As mentioned above, we call a strategy to divide a proof problem by multistep refinement Dividing Strategy. 3
To reduce the difficulty of the simultaneous considerations of (
Parent Evidence PEi branch i Child Evidence CEi1
Child Evidence CEi2
Each branch i in DST also represents refinement step i in Event-B. Suppose that the abstract machine Mi-1 is refined by the concrete machine Mi at refinement step i, we would design Mi so as to meet the child evidences CEij for all j. The definition of the statement "a machine meets an evidence" is given as follows.
Definition 1. An Event-B machine M meets an evidence E if and only if: When E describes a property S, then M has an invariant representing S.
When E describes a behavior B, then M has events representing B.
There are several ways to design a machine so as to represent behaviors. When the evidence consists of pre-condition and post-condition of the behavior, we can introduce an event which has a guard as the pre-condition and an action as the postcondition. Or, when the behavior defines an execution order of events, we can introduce guard conditions into the events to control the order. To completely separate DST from the Event-B formalism, we don't define a formal notation of evidences or direct translation from evidences into machines. Because the parent evidence PEi should also be met in Mi by refinement, any evidences which are met in Mi should be consistent with PEi. Then, CEijs that achieve or implement PEi in DST can come up for the evidences met in Mi. This means DST shows us how many details of the specification should be introduced in Mi, that is, the dividing strategy. Note that if Mi meets all CEijs, it may not satisfy the simulation constraint. Namely, the conjunction of CEijs is not a sufficient but necessary condition for the simulation constraint. 4
In this section, we present the details of our proposed modeling guideline. Conditions. We assume that the following two conditions are satisfied in the guideline: (Cond1) informal specification of the system and the environment has been developed, namely, it is given for Event-B modeling; (Cond2) the safety requirement is informally described as a property in the system specification.
Modeling Procedure. We now describe steps to build an Event-B model. We omit the design of the referred contexts in the procedure.
Step 1. Design the most concrete machine Mk+1 that includes all the details of the given specification.
Step 2. Put the informal safety requirement as the top evidence in the DST. Step 3. Design the machine M0 in which the safety requirement is met. Step 4. In the DST, choose a parent evidence PEi which has no child evidence (called leaf evidence), and develop child evidences CEij which represent given specification or a property deduced from the specification. The child evidences CEij achieve or implement PEi.
Step 5. Refine the machine Mi-1 into the machine Mi. Mi should meet CEij for all j, and also satisfy the simulation constraint. If the simulation constraint can be proved, then go to Step 6. Otherwise, go back to Step 4 to update the DST.
Step 6. If there is a leaf evidence which represents a deduced property, then go to Step 4 for branch i = i + 1. Otherwise, go to Step 7.
Step 7. Refine the machine Mi into the most concrete machine Mk+1. If the simulation constraint can be proved, then terminate the procedure. Otherwise, go back to Step 4.
In our guideline, we also suggest that the most concrete machine Mk+1 should be
designed at the first step based on the informal given specification in order to separate
the consideration (
To confirm the feasibility of our proposed guideline, we have two case studies on a simple file transfer protocol in [1] and switchover mechanism in a fault tolerant system. In this paper, we demonstrate our approach on the case study of the protocol. Specification. As described in [1], the protocol is used by two agents. One agent called sender intends to transfer a sequential file denoted f to the other agent called receiver. The received file is denoted by g. The sequential file is transferred in n items called blocks. The most recent transferred block is denoted by d. The number of times of sending and receiving are denoted by s (s ∈[1..n+1]) and r (r ∈[1..n+1]). Accordingly, the block sent by the sender for the sth time is denoted by f(s). The same applies to g(r). To alternate sending and receiving, the parity bits p and q are introduced. The bit p is inverted with every sending, and the bit q is inverted with every receiving. Step 1. In this case study, we can see the most concrete machine in [1]. Step 2. The safety requirement for the protocol is also defined in [1] as follows. Safety Requirement: After the transfer completes, g is equivalent to f. We also put the requirement description at the top of the DST as shown in Fig. 2. Step 3. The machine M0 is designed to meet the invariant "inv0: r=n+1 ⇒ g=f" that represents the safety requirement. The event receive in M0 is restricted to meet inv0 by the parameters p_g and p_r which denote the next values as follows. receive ≘ any p_g, p_r where grd1:p_r=n+1 ⇒p_g=f, grd2:p_g ∈1‥n ⇸ D, grd3:p_r ∈1‥n+1 then act1:g ≔ p_g, act2:r ≔ p_r end Step 4 for branch 1. The top evidence E0 is chosen as a parent evidence. We develop the evidences E1, E2 and E3 as the child evidences that achieve E0.
Step 5 for branch 1. We refine M0 into M1 so as to meet the evidences E1, E2 and E3. E1 is represented as the invariant inv1 "s=r ∧ r>1 ⇒ 1‥r−1 ◁ g = 1‥s−1 ◁ f". The right side of the symbol "◁" is restricted to the left side. The evidence E2 is represented by the guard grd1 of the event send as below.
send ≘ where grd1:s = r, grd2:s ≠ n + 1 then act1:s ≔ s + 1 end By grd1, the event send occurs only when s is equal to r. The guard grd2 is derived from s ∈ [1..n+1]. We also introduce a similar guard into the event receive for E3. Since M1 designed this way is refined by M0, we can prove the simulation constraint. Step 6 for branch 1. Because there are the leaf evidences E1, E2 and E3 that are deduced from the given specification, we go back to Step 4 for branch 2. Step 4-6 for branch 2. We develop the child evidences E4, E5 and E6 to implement E1. They are introduced into the refined machine M2 as invariants. We choose E2 as the next parent evidence, and then we go back to Step 4 to create the branch 3.
We could similarly design the machine M3 to M7. Finally, we found there is no leaf evidence which represents a deduced property. Then we moved to Step 7. Step 7. We refine the machine M7 into the most concrete machine M8. Since we succeeded in the proof of the simulation constraint, we terminate the modeling.□
Finally, we completed the development of the Event-B model according to the proposed guideline. The completed DST is shown in Fig. 2. The proof statistics of our developments including the other case study is shown in Table 1.
SDaefdeutyceRdeqPuroirpeemrteynt [E0fi]leAgfteisretqhbueritvaranalcenhnsft1etroctohmepolreitgeins,arlefcileeivf.ed Given Specification [E2] Only when s and r are equal, [E3] Only when s is one greater sender can send b than r, receiver can receive b branch 3 branch 4 [E4] After b is transferred, g is equivalent to sent file
except for b branch 5 [E13] Before b is received, g is equivalent to sent file branch 7 [E17] Sending b doesn't change g or sent file [E1] After b is transferred, g is equivalent to sent file branch 2 [E5] After b is transferred, the latest block in g is b [E14] Receiving b doesn't change g and sent file
[E6] After b is transferred, the latest block in sent file is b branch 6 [E7] When sending, [E8] When receiving,
p is inverted q is inverted [E9] When receiving, r is incremented to be equal to s [E10] When p and q are equal, sender can send b [E15] Before b is received, the latest block in sent file is b [E16] Receiving b doesn't change the latest block in sent file or transferred b [E11] When sending, s is incremented to be one greater than r [E12] When p and q
are not equal, receiver can receive b Although refinement is useful for proof, it's not always utilized because of its difficulty. In fact, in the industrial project Dependable Software Forum [13] to popularize Formal Methods in Japan, some people tried Event-B, but didn't use refinement. For those people, we aim to make refinement more accessible and motivating by the separation from Event-B formalism. In particular, we think it's important to present refinement more intuitively in a time-limited lecture or training course. So, we intend to extract the essential part of refinement for developers, which is "how the safety requirement was proved". This encourages them to understand what refinement is, and what impact refinement has on their development. We think one can say the same thing in other formal methods. For example, in a model checking method, the abstraction of the specification should be considered to avoid the state explosion at the same time as the formalization. Similar separations may be effective in the education.
Because one has to follow only the simulation constraint in Event-B refinement,
there are various ways to refine the system. This could be an advantage for experts of
Event-B because they are allowed to develop the model as they like. On the other
hand, that could be a disadvantage for non-experts. In our guideline, we restrict the
modeling approach to top-down by DST. Top-down means to start modeling from the
whole system and divide it into its components. It's also called outside-in approach in
[10], and has been applied in a number of case studies [11] [12]. We think this
restriction is helpful for non-experts because the restriction makes how to start
refinement clearer. However, our guideline is not effective for systems which are not
suitable for the top-down approach. Another limitation is that our guideline only aims to
separate the considerations, but does not solve the difficulties of the considerations
(
There are a number of approaches to take advantage of tree-structured diagrams in
Event-B refinement. In [5], the authors provide a method in which KAOS goal
models [4] are translated into Event-B models. The authors of [7] also propose an
approach to utilize a tree-structured diagram based on KAOS for Event-B refinement.
These methods are similar to our approach in that the parent goal is translated into the
abstract machine, and its child goals are translated into the concrete machine.
However, because they aim for direct translation from goals to machines, the descriptions of
goals are limited to semantically correspond to events of Event-B. This means that
developers have to consider not only (
In contrast, we don't define how to describe evidences in DST, or translation into
Event-B in our approach. This enables us to completely separate (
Another group in [9] works on the traceability between KAOS and Event-B. Since they only use the leaf goals, goal refinement in KAOS doesn't correspond to machine refinement in Event-B, unlike [5], [7] and our approach.
From a more general perspective of refinement support, the work of [6] proposes a
Refinement Planning Sheet to overview refinement. Unlike our approach, it doesn't
intend the separation from Event-B formalism. The authors in [8] also provide an
approach to generate a refinement plan which has the highest evaluation according to
their criteria. However, the generated strategy is not always appropriate. For this
reason, we do not remove, but rather separate, (
In this paper, we presented a modeling guideline to make refinement more accessible
and motivating for developers in learning Event-B. Our approach allows them to
separate (
As future work, we plan to ask developers to try our guideline. We would need to evaluate how accessible and motivating our guideline is in practice in terms of how much time and stress there is in modeling. In addition, comparative evaluation with other related approaches referred to in Section 6 is also important.