# A LTS Approach to Control in Event-B

Authors: Han Peng; Chenglie Du; Lei Rao; Fu Chen
Journal: Scientific Programming
 (2018)

---

## Abstract

In Event-B, people need to use control variables to constrain the order of events, which is a time-consuming and error-prone process. This paper presents a method of combining labeled transition system and iUML-B to complete the behavior modeling of system, which is more convenient and practical for engineers who are accustomed to using the automaton to build a system behavior model. First, we use labeled transition system to establish the behavior model of the system. Then we simulate and verify the event traces of the labeled transition system behavior model. Finally, we convert labeled transition system model into iUML-B state machine and use it to generate the corresponding control flow model. We use Abrial’s bounded retransmission protocol to demonstrate the practicality of our approach. The simulation results show that the system behavior model generated by the iUML-B state machine has the same event trace as the corresponding labeled transition system model.


---

## Body

## 1. Introduction

Event-B [1] is a formal method that evolved from B method [2] and action system [3]. It uses simple symbols and structures to model the system, and it is well suited for different areas including distributed systems [4]. The Event-B method itself is very good at event refinement and data-oriented refinement, but it lacks formal semantics of behavior, and the control flow of Event-B machine is hidden in the state variables, which can enable the event and can be modified by actions. As a result, Event-B machine is not as intuitive as the automaton-based approach.From the designer’s point of view, to constrain the order of events using control variables is a time-consuming and error-prone process. People have to carefully consider the impact of each variable on the event. Control variables and other variables in Event-B machine entangled together, which makes the design process more complex. From the analyst’s point of view, it needs a lot of effort to understand the control flow of system [5]. It is very inconvenient for people who want to understand the overall behavior and verify properties of the system and find the right solution.To summarize, the problem in Event-B control flow is as follows: first, the control flow part and computation part of Event-B machine are entangled, which makes design and analysis more difficult; second, the control flow part is not visible, which makes it impossible to model and verify the control flow separately.In order to solve these two problems, this paper presents a method of modeling, analyzing the control flow of Event-B machines using labeled transition system (LTS). The basic idea is to divide the model into control part and the computation part and further divide the control part into component control flow and interaction control flow. The procedure of our approach is as follows: first, we use LTS to model the component behavior and interaction behavior of the system so that we can visualize the control flow of each component and the entire system (we omit the computation part of the Event-B machine and do not consider it in the control flow model); second, we simulate system behavior using this formal model and get the event trace we need; third, we convert the component behavior LTS and the interaction behavior LTS into the iUML-B component state machine and the control flow state machine, respectively. Finally, we use these iUML-B state machines to generate Event-B machines. We proved in Section2.3 that the Event-B machine generated using the above steps will only preserve those event traces that we need.The remainder of this paper is organized as follows. Section2 summarizes the issues related to Event-B control flow modeling, as well as the general approach we propose. Section 3 uses Abrial’s bounded retransmission protocol to demonstrate the practicality of our approach. Section 4 discusses our approach. Section 5 presents related work and compares the results of this work with existing work. Finally, Section 6 concludes the paper and gives some future research directions.


## 2. Methodological Approach

### 2.1. Problem Description

We use Abrial’s bounded retransmission protocol (BRP) model [1] to explain the control flow problems in Event-B machine. In the fourth refinement model of BRP machine (the example can be found at http://www.math.pku.edu.cn/teachers/jrabrial/course/BRP.zip), there are multiple control variables that affect the event order, as Figure 1 shows.Figure 1
The control variables of Event-B machine.To simplify the problem, we omit the variables that do not affect the event order of Event-B machine. In Figure1, we mark the position of these variables in italics. Now, if we want to analyze the effect of Boolean variable W on the event order, we will find that the eventSND_snd_data changes the value of W from TRUE to FALSE, which will affect all the other events in the graph (we only list events affected by W), as indicated by the dashed arrows. But this does not mean that when W is FALSE, the other events will be enabled. In fact, the occurrence of other events depends on the value of more control variables, such ass_st andr_st etc. Therefore, in order to analyze the effect of W on the event order, we have to put these events together in a graph so that we can understand the intention of the modeler.


### 2.2. Control the Event-B Machine Using iUML-B State Machine

iUML-B [6, 7] is a graphical plug-in of Event-B, which use “UML like" class diagrams and state machines to describe the state and behavior of system. The iUML-B’s graphical model can generate Event-B code directly on the Rodin platform [8] and automatically embed the generated code into the context part (set, constant, and axiom) and machine parts (variables, events, and invariants).The transform edges in the iUML-B state machine can be “linked" to the events in the Event-B machine to control the event order in Event-B machine. The principle is shown in Figure2.Figure 2
iUML-B state machine control flow modeling principle.For example, if we want to restrict the event order in the Event-B machine as<INITIALISATION, SND_snd_data, RCV_current_data, SND_rcv_current_ack, brp>,we can first draw the iUML-B state machine shown in Figure2; then “link” each transition edge to an event to make the events in the Event-B machine occur in the order specified in the iUML-B state machine.Although the iUML-B state machine can model the control flow of the Event-B machine, it lacks formal behavioral semantics. Therefore, we need to use LTS to model and analyze its behavior.


### 2.3. Behavior Modeling Strategy and Equivalence Proving

We present the following Event-B machine behavior modeling strategy based on the above analysis results:(1)
The system requirements are decomposed into component requirements and control flow requirements, where component requirements represent the constraints of the event order of a component itself and the flow requirements represent the event order between components.(2)
The behavior LTS of each component, which contains only the events that occurred in the component itself and the local variables of the component itself, is established according to the component requirements.(3)
The system control flow LTS, which describes event order between multiple components, is established according to the control flow requirements.(4)
The component LTS and control flow LTS are composed to establish the system LTS. Then we can simulate and analyze the event traces of the system LTS in the LTSA [9] environment and modify it until it satisfies our requirements.(5)
A component LTS is mapped onto an iUML-B state machine (we call it the component state machine). A system control flow LTS is mapped onto an iUML-B state machine (we call it the flow state machine), too.(6)
The Event-B machine which meets our requirements is generated using the component state machine and flow state machine.The proposed modeling process is shown in Figure3.Figure 3
Event-B machine behavior modeling strategy.In order to prove the correctness of our method, we give a complete proof of bisimulation equivalence between the LTS system and Event-B model. We first give the definition of LTS and its composition.Definition 1 (LTS).
LetStates represent a universal set of states,Acts represents a universal action set, and then a LTS P is defined as a quaternion P=Q,Σ,Δ,q, where(i)
Q⊆States, representing the state set of P;(ii)
Σ=αP(αP⊆Acts), representing the action set of P;(iii)
Δ⊆Q×Σ×Q, representing the transition relationship in P; these transitions are labeled with the elements in Σ;(iv)
q∈Q, representing the initial state of P.We need to use the parallel composition of LTSs to express the interaction between multiple LTSs. The following gives the definition of LTS parallel composition.Definition 2 (parallel composition of LTSs).
The parallel composition of twoLTSM=Q1,Σ1,Δ1,q1 and N=Q2,Σ2,Δ2,q2 is expressed as LTS(M∥N)=Q1×Q2,Σ1∪Σ2,Δ,(q1,q2), where Δ is the minimum relation that satisfies the following constraint:(1)M→aM′M∥N→aM′∥Na∉αN(2)N→aN′M∥N→aM∥N′a∉αM(3)M→aM′,N→aN′M∥N→aM′∥N′a≠τ,where a∈Σ1∪Σ2, τ represents an internal action that is not visible to the outside.We use the bisimulation definition in the literature [10].Definition 3 (bisimulation equivalent).
LetLTSi=(Qi,Σi,Δi,qi), i=1,2, be labeled transition systems over the set Σ of actions. Anbisimulation for (LTS1,LTS2) is a binary relation R⊆Q1×Q2 such that(A)
for the initial stateq1 and q2, (q1,q2)∈R(B)
for any(s1,s2)∈R it holds that(1)
ifs1→a1s1′, then s2→a2s2′ with (s1′,s2′,)∈R for some s2′∈Q2(2)
ifs2→a2s2′, then s1→a1s1′ with (s1′,s2′,)∈R for some s1′∈Q1
L T S 1 and LTS2 arebisimulation equivalent (or bisimilar), denoted as LTS1~LTS2, if there exists an bisimulation R for (LTS1,LTS2). The bisimulation equivalence relationship is transmitted, i.e., LTS1~LTS2∧LTS2~LTS3⟹LTS1~LTS3.We collectively refer to component LTS and control flow LTS as “atomic LTS." The state of each “atomic LTS" is the state of a single variable, not the composition of other LTSs. Therefore, a system’s LTS is a composition of multiple atomic LTSs:(4)LTSsystem=∥i=1nAtomicLTSi,where “∥" is the LTS composition operator, i is the sequence number of the atomic LTS, and n is the total number of atomic LTSs.The proof process is as follows.(1) We first establish an “atomic iUML-B state machine" based on the atomic LTSAtomicLTS=Q,Σ,Δ,q. The construction process of atomic iUML-B state machine is as follows.(a) An “atomic iUML-B state machine" is defined asAtomicStm=Node,E,Edge,InitNode, where Node represents a set of nodes in the iUML-B state machine; E represents the set of events that linked on the iUML-B state machine’s edge. Edge⊆Node×E×Node represents the set of edges in the iUML-B state machine;InitNode represents the initial node of the iUML-B state machine, which is the target node of the edge that is linked to theInitialization event.(b) In the process of establishing the atomic iUML-B state machine, letNode=Q, E=Σ, Edge=Δ, InitNode=q. For example, if there is a state s1 (transition t) inAtomicLTS, a node s1 (edge e) is also drawn in the corresponding “atomic iUML-B state machine." This mapping process is very easy to operate and we will not explain it further.(c) Generate the Event-B code for this atomic iUML-B state machine using the automatic code generation tool of the Rodin platform.(2) In the following we prove that the Event-B model generated byAtomicStm is bisimulation equivalent toAtomicLTS.We define an Event-B model asM=V,Event,Guard,Action,Vinit, where V represents variables set of M, Event represents event set of M, Guard represents guard set of M, Action represents action set of M, and Vinit represents the initial value set for each element in the V. We define the LTS corresponding to the M as LTS(M)=(QM,ΣM,ΔM,qM).We named an Event-B model generated byAtomicStm as MA=VA,EventA,GuardA,ActionA,VinitA. It should be emphasized that at this time there is only one element v in VA, and VinitA is the initial value of v (because anAtomicStm only describes the change of one variable). EventA represents events that modify the value of v, and GuardA represents those guards that contain v in thewhen clause of an event. Similarly, ActionA represents actions that modify the value of v. We assume that the type of v is D, that is, v∈D; then the state space of v is D.SinceMA’s code is generated byAtomicStm, we have LTS(AtomicStm)~LTS(MA)=(QMA,ΣMA,ΔMA,qMA). If an Event-B model M is composed of multiple atomic iUML-B states machine generated together, then we have(5)LTSM=∥i=1nLTSMAi,where i is the sequence number of the atomic iUML-B state machine, and n is the total number of atomic iUML-B state machines.We explain the equivalence betweenAtomicLTS and MA according to Rodin’s rules for generating Event-B code from the iUML-B state machine.(a) First, Rodin will generate a variable based onone AtomicStm and automatically generate aSET which contains all possible values of this variable. For example, anAtomicStm named “node" which contains n nodes (e.g., s1,s2,…,sn) will generate(6)partitionNode,s1,s2,…,snwhich means node∈Node. As we mentioned in (1) (b), Node=Q. Therefore, the state space D of variable “node” of Event-B model MA is equal to Q, and then QMA=Q.(b) Secondly, Rodin generates the following code based on the edge that links theInitialization event:(7)INITIALISATION≙BEGINnode=s1ENDSince s1 = q (in the construction process (1) (b)), we have Vinit=q, and then qMA=q.(c) Rodin will generate an event named “event_i” in the Event-B model MA according to the event “event_i” which has been linked on the edge of iUML-B state machine, and will generate the following code according to each edge from the node si to sj (where si and sj are the node name):(8)event_i≙when  node=sithen  node≔sjTherefore, for a transition si→asj inAtomicLTS, there will be a corresponding transition si→event_isj in LTS(MA). At the same time, for each action a inAtomicLTS, there will be an event event_i corresponding to it in the Event-B model MA. So we have ΔMA=Δ.(d) The reverse mapping process fromMA toAtomicLTS is similar, and we will not repeat them here.(e) We can define a mapping relationshipR so thatAtomicLTS and LTS (MA) comply with the requirement of bisimulation equivalence. In fact, this R can be a renamed function, such as R (Sender) = sender; now we get (9)LTSAtomicStm~LTSMA~AtomicLTS(3) Finally, we use the theorem in the literature [10].Lemma 4 (congruence w.r.t LTS composition).
For labeled transition systemsLTS1 and LTS1′ over Σ1, LTS2 and LTS2′ over Σ2, and H⊆Σ1∩Σ2, it holds that (10)LTS1~LTS1′,LTS2~LTS2′impliesLTS1∥HLTS1′~LTS2∥HLTS2′According to expression (4) and expression (5) and Lemma 4, we have(11)∥i=1nLTSMAi~∥i=1nAtomicLTSiThat is, the LTS model LTS (System) of the system and the LTS modelLTS(M) of Event-B model obtained according to the mapping rule of (1) are bisimulation equivalent:(12)LTSM~LTSsystem.


## 2.1. Problem Description

We use Abrial’s bounded retransmission protocol (BRP) model [1] to explain the control flow problems in Event-B machine. In the fourth refinement model of BRP machine (the example can be found at http://www.math.pku.edu.cn/teachers/jrabrial/course/BRP.zip), there are multiple control variables that affect the event order, as Figure 1 shows.Figure 1
The control variables of Event-B machine.To simplify the problem, we omit the variables that do not affect the event order of Event-B machine. In Figure1, we mark the position of these variables in italics. Now, if we want to analyze the effect of Boolean variable W on the event order, we will find that the eventSND_snd_data changes the value of W from TRUE to FALSE, which will affect all the other events in the graph (we only list events affected by W), as indicated by the dashed arrows. But this does not mean that when W is FALSE, the other events will be enabled. In fact, the occurrence of other events depends on the value of more control variables, such ass_st andr_st etc. Therefore, in order to analyze the effect of W on the event order, we have to put these events together in a graph so that we can understand the intention of the modeler.


## 2.2. Control the Event-B Machine Using iUML-B State Machine

iUML-B [6, 7] is a graphical plug-in of Event-B, which use “UML like" class diagrams and state machines to describe the state and behavior of system. The iUML-B’s graphical model can generate Event-B code directly on the Rodin platform [8] and automatically embed the generated code into the context part (set, constant, and axiom) and machine parts (variables, events, and invariants).The transform edges in the iUML-B state machine can be “linked" to the events in the Event-B machine to control the event order in Event-B machine. The principle is shown in Figure2.Figure 2
iUML-B state machine control flow modeling principle.For example, if we want to restrict the event order in the Event-B machine as<INITIALISATION, SND_snd_data, RCV_current_data, SND_rcv_current_ack, brp>,we can first draw the iUML-B state machine shown in Figure2; then “link” each transition edge to an event to make the events in the Event-B machine occur in the order specified in the iUML-B state machine.Although the iUML-B state machine can model the control flow of the Event-B machine, it lacks formal behavioral semantics. Therefore, we need to use LTS to model and analyze its behavior.


## 2.3. Behavior Modeling Strategy and Equivalence Proving

We present the following Event-B machine behavior modeling strategy based on the above analysis results:(1)
The system requirements are decomposed into component requirements and control flow requirements, where component requirements represent the constraints of the event order of a component itself and the flow requirements represent the event order between components.(2)
The behavior LTS of each component, which contains only the events that occurred in the component itself and the local variables of the component itself, is established according to the component requirements.(3)
The system control flow LTS, which describes event order between multiple components, is established according to the control flow requirements.(4)
The component LTS and control flow LTS are composed to establish the system LTS. Then we can simulate and analyze the event traces of the system LTS in the LTSA [9] environment and modify it until it satisfies our requirements.(5)
A component LTS is mapped onto an iUML-B state machine (we call it the component state machine). A system control flow LTS is mapped onto an iUML-B state machine (we call it the flow state machine), too.(6)
The Event-B machine which meets our requirements is generated using the component state machine and flow state machine.The proposed modeling process is shown in Figure3.Figure 3
Event-B machine behavior modeling strategy.In order to prove the correctness of our method, we give a complete proof of bisimulation equivalence between the LTS system and Event-B model. We first give the definition of LTS and its composition.Definition 1 (LTS).
LetStates represent a universal set of states,Acts represents a universal action set, and then a LTS P is defined as a quaternion P=Q,Σ,Δ,q, where(i)
Q⊆States, representing the state set of P;(ii)
Σ=αP(αP⊆Acts), representing the action set of P;(iii)
Δ⊆Q×Σ×Q, representing the transition relationship in P; these transitions are labeled with the elements in Σ;(iv)
q∈Q, representing the initial state of P.We need to use the parallel composition of LTSs to express the interaction between multiple LTSs. The following gives the definition of LTS parallel composition.Definition 2 (parallel composition of LTSs).
The parallel composition of twoLTSM=Q1,Σ1,Δ1,q1 and N=Q2,Σ2,Δ2,q2 is expressed as LTS(M∥N)=Q1×Q2,Σ1∪Σ2,Δ,(q1,q2), where Δ is the minimum relation that satisfies the following constraint:(1)M→aM′M∥N→aM′∥Na∉αN(2)N→aN′M∥N→aM∥N′a∉αM(3)M→aM′,N→aN′M∥N→aM′∥N′a≠τ,where a∈Σ1∪Σ2, τ represents an internal action that is not visible to the outside.We use the bisimulation definition in the literature [10].Definition 3 (bisimulation equivalent).
LetLTSi=(Qi,Σi,Δi,qi), i=1,2, be labeled transition systems over the set Σ of actions. Anbisimulation for (LTS1,LTS2) is a binary relation R⊆Q1×Q2 such that(A)
for the initial stateq1 and q2, (q1,q2)∈R(B)
for any(s1,s2)∈R it holds that(1)
ifs1→a1s1′, then s2→a2s2′ with (s1′,s2′,)∈R for some s2′∈Q2(2)
ifs2→a2s2′, then s1→a1s1′ with (s1′,s2′,)∈R for some s1′∈Q1
L T S 1 and LTS2 arebisimulation equivalent (or bisimilar), denoted as LTS1~LTS2, if there exists an bisimulation R for (LTS1,LTS2). The bisimulation equivalence relationship is transmitted, i.e., LTS1~LTS2∧LTS2~LTS3⟹LTS1~LTS3.We collectively refer to component LTS and control flow LTS as “atomic LTS." The state of each “atomic LTS" is the state of a single variable, not the composition of other LTSs. Therefore, a system’s LTS is a composition of multiple atomic LTSs:(4)LTSsystem=∥i=1nAtomicLTSi,where “∥" is the LTS composition operator, i is the sequence number of the atomic LTS, and n is the total number of atomic LTSs.The proof process is as follows.(1) We first establish an “atomic iUML-B state machine" based on the atomic LTSAtomicLTS=Q,Σ,Δ,q. The construction process of atomic iUML-B state machine is as follows.(a) An “atomic iUML-B state machine" is defined asAtomicStm=Node,E,Edge,InitNode, where Node represents a set of nodes in the iUML-B state machine; E represents the set of events that linked on the iUML-B state machine’s edge. Edge⊆Node×E×Node represents the set of edges in the iUML-B state machine;InitNode represents the initial node of the iUML-B state machine, which is the target node of the edge that is linked to theInitialization event.(b) In the process of establishing the atomic iUML-B state machine, letNode=Q, E=Σ, Edge=Δ, InitNode=q. For example, if there is a state s1 (transition t) inAtomicLTS, a node s1 (edge e) is also drawn in the corresponding “atomic iUML-B state machine." This mapping process is very easy to operate and we will not explain it further.(c) Generate the Event-B code for this atomic iUML-B state machine using the automatic code generation tool of the Rodin platform.(2) In the following we prove that the Event-B model generated byAtomicStm is bisimulation equivalent toAtomicLTS.We define an Event-B model asM=V,Event,Guard,Action,Vinit, where V represents variables set of M, Event represents event set of M, Guard represents guard set of M, Action represents action set of M, and Vinit represents the initial value set for each element in the V. We define the LTS corresponding to the M as LTS(M)=(QM,ΣM,ΔM,qM).We named an Event-B model generated byAtomicStm as MA=VA,EventA,GuardA,ActionA,VinitA. It should be emphasized that at this time there is only one element v in VA, and VinitA is the initial value of v (because anAtomicStm only describes the change of one variable). EventA represents events that modify the value of v, and GuardA represents those guards that contain v in thewhen clause of an event. Similarly, ActionA represents actions that modify the value of v. We assume that the type of v is D, that is, v∈D; then the state space of v is D.SinceMA’s code is generated byAtomicStm, we have LTS(AtomicStm)~LTS(MA)=(QMA,ΣMA,ΔMA,qMA). If an Event-B model M is composed of multiple atomic iUML-B states machine generated together, then we have(5)LTSM=∥i=1nLTSMAi,where i is the sequence number of the atomic iUML-B state machine, and n is the total number of atomic iUML-B state machines.We explain the equivalence betweenAtomicLTS and MA according to Rodin’s rules for generating Event-B code from the iUML-B state machine.(a) First, Rodin will generate a variable based onone AtomicStm and automatically generate aSET which contains all possible values of this variable. For example, anAtomicStm named “node" which contains n nodes (e.g., s1,s2,…,sn) will generate(6)partitionNode,s1,s2,…,snwhich means node∈Node. As we mentioned in (1) (b), Node=Q. Therefore, the state space D of variable “node” of Event-B model MA is equal to Q, and then QMA=Q.(b) Secondly, Rodin generates the following code based on the edge that links theInitialization event:(7)INITIALISATION≙BEGINnode=s1ENDSince s1 = q (in the construction process (1) (b)), we have Vinit=q, and then qMA=q.(c) Rodin will generate an event named “event_i” in the Event-B model MA according to the event “event_i” which has been linked on the edge of iUML-B state machine, and will generate the following code according to each edge from the node si to sj (where si and sj are the node name):(8)event_i≙when  node=sithen  node≔sjTherefore, for a transition si→asj inAtomicLTS, there will be a corresponding transition si→event_isj in LTS(MA). At the same time, for each action a inAtomicLTS, there will be an event event_i corresponding to it in the Event-B model MA. So we have ΔMA=Δ.(d) The reverse mapping process fromMA toAtomicLTS is similar, and we will not repeat them here.(e) We can define a mapping relationshipR so thatAtomicLTS and LTS (MA) comply with the requirement of bisimulation equivalence. In fact, this R can be a renamed function, such as R (Sender) = sender; now we get (9)LTSAtomicStm~LTSMA~AtomicLTS(3) Finally, we use the theorem in the literature [10].Lemma 4 (congruence w.r.t LTS composition).
For labeled transition systemsLTS1 and LTS1′ over Σ1, LTS2 and LTS2′ over Σ2, and H⊆Σ1∩Σ2, it holds that (10)LTS1~LTS1′,LTS2~LTS2′impliesLTS1∥HLTS1′~LTS2∥HLTS2′According to expression (4) and expression (5) and Lemma 4, we have(11)∥i=1nLTSMAi~∥i=1nAtomicLTSiThat is, the LTS model LTS (System) of the system and the LTS modelLTS(M) of Event-B model obtained according to the mapping rule of (1) are bisimulation equivalent:(12)LTSM~LTSsystem.


## 3. BRP Case Study

In this section, we take Abrial’s BRP protocol model in Chapter6 of [1] as an example. We use our proposed method to establish the system component model and control flow model step by step and finally get a BRP protocol control flow model in Event-B.


### 3.1. System Overview

The purpose of BRP is to transfer sequential files from the sender to the receiver. After the transfer is complete, the recipient’s file should be equal to the sender’s original file. The sender should split the files that need to be sent into a series of data blocks and send the data blocks to the receiver in order. Once the receiver receives the data item, it stores it in its own file and sends an acknowledgement message to the sender on an acknowledgement channel. The sender will send the next data item after receiving this acknowledgement message. The principle of the BRP protocol is shown in Figure4.Figure 4
The principle of bounded retransmission protocol.At the beginning of modeling process, there are only two components in the system, Sender and Receiver. During the refinement process, we add the new event and component LTS to model; then we add control flow LTS according to the flow requirement. We present the events and requirements for each level of refinement, as shown in Table1.Table 1
System requirements.
Introduced Events System Requirements. Level0 SND_progress,RCV_progress,brp Component Requirements  Com0.1: The event brp cannot occur unless the sender has completed the event SND_progress.Com0.2: The event brp cannot occur unless the event RCV_progress has been completed.Flow Requirements  Flow0.1: SND_progress, and RCV_progress can occur interleaving in arbitrary.Flow0.2: The event brp cannot occur unless events SND_progress and RCV_progress have both completed.  Level1 SND_success,SND_failure,RCV_success,RCV_failure. Component Requirements  Com1.1: After the sender is initialized, it may send successfully or may fail to send, and then the brp event occurs.Com1.2: After the receiver is initialized, it may be successful to receive or fail to receive, and then the brp event occurs.Flow Requirements  Flow1.1: When the system is initialized, only event SND_failure or RCV_success can occur.Flow1.2: Sender failed event will cause the receiver to fail.Flow1.3: Receiver succeed event will cause the sender to succeed.  Level2 RCV_rcv_current_data Component Requirements  Com2.1: If the received data is not the last data, the event RCV_current_data occurs. If the received data is the last data, the event RCV_success occurs.  Level3 SND_snd_data,SND_timeout,SND_rcv_curr_ack Component Requirements  Com3.1: The event SND_snd_data occurs if the message to be sent is not the last message.Com3.2: If the message to be sent is the last message, the event SND_success occurs.Com3.3: The sender may receive an acknowledgement message only after the data has been sent.Com3.4: After sending the data, the sender may occur a time out event because the acknowledgment message has not been received.Com3.5: The sender will send the next data after receiving the acknowledgment message.Com3.6: The sender will send the current data again after a time out event occurs.Flow Requirements  Flow3.1: The receiver may accept the current data only after the sender has sent the data.Flow3.2: After the sender sends the data, the event RCV_success may occur (that is, accept the last data).


### 3.2. Modeling Process

In the modeling process, we represent component LTS withSN,RN (N is the refinement level) and represent the flow requirement withFlowM (M is the requirement number). The iUML-B component state machine is represented withSNDMachineN,RCVMachineN (N is the refinement level), and the iUML-B control flow state machine is represented withFlowM (M is the flow requirement number). We use finite state process (FSP) [9] to represent the LTS and use LTSA tool to simulate and verify the LTS.FSP (finite state processes) is a process algebra that can describe LTS. The FSP operators used in this paper are as follows.(1) Order: “->”, indicating the order of the action, such asx -> P means that the action x is executed first, and the action sequence described by the process P is executed.(2) Select: “∣”, that is, the choice of different execution actions, such asx -> P ∣ y -> Q said: the first action x, and then follow the description of P; or the first action y, and then follow the description of Q.(3) Recursion: the behavior of a process may be defined in terms of itself, in order to express repetition.(4) End state:“END”: describes a process that has terminated successfully and cannot perform any more actions.(5) Condition control: “when”, that in given conditions to perform a certain action, such aswhenBx->P∣y->Q said: if the condition B is established, in addition to y -> Q can choose to perform action x and then execute the action sequence of process P; if B is not established, only the action y can be executed, and then the action sequence of process Q is executed. Here, B is a state predicate.(6) Parallel composition: “∥”, representing a composition of multiple simple processes, such asP∥Q means that the sequence of actions in processes P and Q is executed concurrently where P and Q are also called subprocesses.System Abstraction Model. The system abstract model includes only three events, which represent the sender’s action(SND_progress), the receiver’s action(RCV_progress), and the communication completion event (brp), respectively. We build the sender and the receiver’s component LTS according to Com0.1 and Com0.2, as shown in Figures 5(a) and 5(b). The corresponding FSP is expressed as (in FSP, action names cannot start with uppercase letters, so we can only express actions with lowercase letters. The mapping rule is:snd_XXX action in FSP corresponds to eventSND_XXX in Event-B):S0 = (snd_progress-> BRP), BRP = (brp-> END).R0 = (rcv_progress-> BRP), BRP = (brp-> END).Figure 5
The LTS of the abstract model and the composition of the component LTS.
(a)
LTS S0 (b)
LTS R0 (c)
LTS Sys0We found that the composition of the sender component LTS and the receiver component LTS was able to meet the flow requirements of Flow 0.1 and Flow 0.2, so we did not need to add any control flow LTS. We get the system LTS of abstract model using LTS composition; as Figure5(c) shown, the FSP expression is∥Sys0 = (S0 ∥R0).We map the Level0 LTS model onto the iUML-B state machine and get the two state machines as shown in Figure6.Figure 6
System abstract model in iUML-B.
(a)
SNDMachine0 (b)
RCVMachine0First Refinement. For the introduced events of the first refinement, we first add them to the two component LTS according to Com1.1 and Com1.2, as shown in Figures 7(a) and 7(b). The FSP code isR1 = (rcv_success->Rsucc∣rcv_failure->Rfail), Rsucc = (brp-> END), Rfail = (brp-> END).S1 = (snd_success->Ssucc∣snd_failure->Sfail), Ssucc = (brp-> END), Sfail = (brp-> END).Figure 7
The component LTSs and flow LTSs of the first refinement model.
(a)
LTS S1 (b)
LTS R1 (c)
LTS Flow1 (d)
LTS Flow2Flow1.2 and Flow1.3 constrain the enable relationship between the sender and the receiver in the first refinement, while Flow1.1 constrains which event occurs first when the system is initialized. Combined with these three flow requirements, we get the control flow LTS as Figures7(c) and 7(d) show. The FSP code isFlow1 = (rcv_success->snd_success->Flow1).Flow2 = (snd_failure->rcv_failure->Flow2).It should be noted that LTS Flow1 not only restricts that a sender’s failure will cause a receiver’s failure, but also restricts that when the system is initialized, only the eventsnd_failure may occur. If we putrcv_failure before the eventsnd_failure in LTS Flow1, this LTS will violate the flow requirement. We get the system-level LTS of Level1 as shown in Figure 8, and its FSP expression is∥Sys1 =(S1∥R1∥Flow1∥Flow2).Figure 8
The system LTS of first refinement.We map the LTS models of Level1 to the iUML-B state machine and get the four state machines as shown in Figure9, whereSNDMachine1 andRCVMachine1 are the component state machines of the sender and receiver, respectively, and Flow1 and Flow2 correspond to LTS Flow1 and LTS Flow2, respectively.Figure 9
iUML-B state machines of first refinement.
(a)
SNDMachine1 (b)
RCVMachine1 (c)
Flow1 state machine (d)
Flow2 state machineSecond Refinement. The second level refinement only introduces one eventrcv_current_data, which does not involve the flow requirement associated with the sender, so we do not need to modify the sender component but only need to add eventrcv_current_data to the receiver’s component LTS, as Figure 10(b) shows. The FSP code isconst N = 2range T = 0⋯NR2=R2[0],R2 [r: T] = (when (r + 1 <N) rcv_current_data [r] -> R2 [r + 1]∣when (r + 1 == N) rcv_success->Rsucc∣rcv_failure->Rfail),Rsucc = (brp-> END),Rfail = (brp-> END).Figure 10
The iUML-B state machine RCVMachine2 and LTS R2.
(a)
RCVMachine2 (b)
LTS R2In the above codes, we introduce the message counterr of the receiver which represents the number of messages currently received. The constant N represents the total number of messages.We map Level2’s LTS model to the iUML-B state machine and get the new receiver state machine as shown in Figure10(a).In addition, we find thatr is a newly introduced variable, so we must model its changes using a new atomic LTS. We introduce a new atomic LTS RCV_QUEUE to express the change of r:RCV_QUEUE = RCV_QUEUE [0][0],RCV_QUEUE [s:T][r:T] = (when (r+1<N) rcv_current_data ->RCV_QUEUE [s][r+1]∣when (r+1==N)rcv_success-> RCV_QUEUE [s][r+1]).The LTS and the corresponding iUML-B state machine ofRCV_QUEUE are shown in Figure 11.Figure 11
The LTS and the corresponding iUML-B state machine ofRCV_QUEUE.
(a)
Rcv_queue state machine (b)
LTS Rcv_queueThis system-level LTS of level2 is shown in Figure12; the FSP expression is∥Sys2 =(S2 ∥R2 ∥Flow1 ∥Flow2 ∥RCV_QUEUE),Figure 12
The system LTS of second refinement.whereS2 =S1.At this level of refinement, there are no changes in the sender’s LTS and control flow LTS, so we do not need to modify the corresponding iUML-B state machine.Due to space limitations, we omitted the description of LTS model and iUML-B state machine model of the third layer refinement.


### 3.3. Property Verification of the Event-B Model

We use the iUML-B state machine to generate the BRP protocol control flow model in Event-B. These automatically generated control flow models have covered all the control variables of the fourth layer of Abiral’s BRP model. Thanks for iUML-B, we can refine the original component state machine and the flow state machine by adding new substates in the original state in the refinement of each layer and preserve the consistency of the Event-B model by refinement checks to ensure that concrete machine is the effective refinement of abstract machine.As we proved in Section2.3, the Event-B model we constructed is bisimulation equivalent to the original LTS model. Therefore, we can verify the properties of the Event-B model by verifying the properties of the original LTS model. We formalized the requirements of the BRP system of Table 1 using linear temporal logic (LTL) formulate; some of them are shown in Table 2. In Table 2, the symbol “□”, “U”, and “◇” represent “always”, “until”, and “eventually” in linear temporal logic, respectively, while the symbols “→”, “¬” and “∧” represent “implication”, “negative”, and “conjunction” in proposition logic, respectively.Table 2
The LTL formulate of basic requirements.
Requirement number LTL formulate Com0.1, Com0.2, Flow0.2 □(¬brp U (snd_progress∧rcv_progress)) Flow1.2 □(snd_failure→◇rcv_failure) Flow1.3 □(rcv_success→◇snd_success)We verified these properties with the help of the LTSA tool and the results show that the behavior of our model meets the requirements in Table1.


## 3.1. System Overview

The purpose of BRP is to transfer sequential files from the sender to the receiver. After the transfer is complete, the recipient’s file should be equal to the sender’s original file. The sender should split the files that need to be sent into a series of data blocks and send the data blocks to the receiver in order. Once the receiver receives the data item, it stores it in its own file and sends an acknowledgement message to the sender on an acknowledgement channel. The sender will send the next data item after receiving this acknowledgement message. The principle of the BRP protocol is shown in Figure4.Figure 4
The principle of bounded retransmission protocol.At the beginning of modeling process, there are only two components in the system, Sender and Receiver. During the refinement process, we add the new event and component LTS to model; then we add control flow LTS according to the flow requirement. We present the events and requirements for each level of refinement, as shown in Table1.Table 1
System requirements.
Introduced Events System Requirements. Level0 SND_progress,RCV_progress,brp Component Requirements  Com0.1: The event brp cannot occur unless the sender has completed the event SND_progress.Com0.2: The event brp cannot occur unless the event RCV_progress has been completed.Flow Requirements  Flow0.1: SND_progress, and RCV_progress can occur interleaving in arbitrary.Flow0.2: The event brp cannot occur unless events SND_progress and RCV_progress have both completed.  Level1 SND_success,SND_failure,RCV_success,RCV_failure. Component Requirements  Com1.1: After the sender is initialized, it may send successfully or may fail to send, and then the brp event occurs.Com1.2: After the receiver is initialized, it may be successful to receive or fail to receive, and then the brp event occurs.Flow Requirements  Flow1.1: When the system is initialized, only event SND_failure or RCV_success can occur.Flow1.2: Sender failed event will cause the receiver to fail.Flow1.3: Receiver succeed event will cause the sender to succeed.  Level2 RCV_rcv_current_data Component Requirements  Com2.1: If the received data is not the last data, the event RCV_current_data occurs. If the received data is the last data, the event RCV_success occurs.  Level3 SND_snd_data,SND_timeout,SND_rcv_curr_ack Component Requirements  Com3.1: The event SND_snd_data occurs if the message to be sent is not the last message.Com3.2: If the message to be sent is the last message, the event SND_success occurs.Com3.3: The sender may receive an acknowledgement message only after the data has been sent.Com3.4: After sending the data, the sender may occur a time out event because the acknowledgment message has not been received.Com3.5: The sender will send the next data after receiving the acknowledgment message.Com3.6: The sender will send the current data again after a time out event occurs.Flow Requirements  Flow3.1: The receiver may accept the current data only after the sender has sent the data.Flow3.2: After the sender sends the data, the event RCV_success may occur (that is, accept the last data).


## 3.2. Modeling Process

In the modeling process, we represent component LTS withSN,RN (N is the refinement level) and represent the flow requirement withFlowM (M is the requirement number). The iUML-B component state machine is represented withSNDMachineN,RCVMachineN (N is the refinement level), and the iUML-B control flow state machine is represented withFlowM (M is the flow requirement number). We use finite state process (FSP) [9] to represent the LTS and use LTSA tool to simulate and verify the LTS.FSP (finite state processes) is a process algebra that can describe LTS. The FSP operators used in this paper are as follows.(1) Order: “->”, indicating the order of the action, such asx -> P means that the action x is executed first, and the action sequence described by the process P is executed.(2) Select: “∣”, that is, the choice of different execution actions, such asx -> P ∣ y -> Q said: the first action x, and then follow the description of P; or the first action y, and then follow the description of Q.(3) Recursion: the behavior of a process may be defined in terms of itself, in order to express repetition.(4) End state:“END”: describes a process that has terminated successfully and cannot perform any more actions.(5) Condition control: “when”, that in given conditions to perform a certain action, such aswhenBx->P∣y->Q said: if the condition B is established, in addition to y -> Q can choose to perform action x and then execute the action sequence of process P; if B is not established, only the action y can be executed, and then the action sequence of process Q is executed. Here, B is a state predicate.(6) Parallel composition: “∥”, representing a composition of multiple simple processes, such asP∥Q means that the sequence of actions in processes P and Q is executed concurrently where P and Q are also called subprocesses.System Abstraction Model. The system abstract model includes only three events, which represent the sender’s action(SND_progress), the receiver’s action(RCV_progress), and the communication completion event (brp), respectively. We build the sender and the receiver’s component LTS according to Com0.1 and Com0.2, as shown in Figures 5(a) and 5(b). The corresponding FSP is expressed as (in FSP, action names cannot start with uppercase letters, so we can only express actions with lowercase letters. The mapping rule is:snd_XXX action in FSP corresponds to eventSND_XXX in Event-B):S0 = (snd_progress-> BRP), BRP = (brp-> END).R0 = (rcv_progress-> BRP), BRP = (brp-> END).Figure 5
The LTS of the abstract model and the composition of the component LTS.
(a)
LTS S0 (b)
LTS R0 (c)
LTS Sys0We found that the composition of the sender component LTS and the receiver component LTS was able to meet the flow requirements of Flow 0.1 and Flow 0.2, so we did not need to add any control flow LTS. We get the system LTS of abstract model using LTS composition; as Figure5(c) shown, the FSP expression is∥Sys0 = (S0 ∥R0).We map the Level0 LTS model onto the iUML-B state machine and get the two state machines as shown in Figure6.Figure 6
System abstract model in iUML-B.
(a)
SNDMachine0 (b)
RCVMachine0First Refinement. For the introduced events of the first refinement, we first add them to the two component LTS according to Com1.1 and Com1.2, as shown in Figures 7(a) and 7(b). The FSP code isR1 = (rcv_success->Rsucc∣rcv_failure->Rfail), Rsucc = (brp-> END), Rfail = (brp-> END).S1 = (snd_success->Ssucc∣snd_failure->Sfail), Ssucc = (brp-> END), Sfail = (brp-> END).Figure 7
The component LTSs and flow LTSs of the first refinement model.
(a)
LTS S1 (b)
LTS R1 (c)
LTS Flow1 (d)
LTS Flow2Flow1.2 and Flow1.3 constrain the enable relationship between the sender and the receiver in the first refinement, while Flow1.1 constrains which event occurs first when the system is initialized. Combined with these three flow requirements, we get the control flow LTS as Figures7(c) and 7(d) show. The FSP code isFlow1 = (rcv_success->snd_success->Flow1).Flow2 = (snd_failure->rcv_failure->Flow2).It should be noted that LTS Flow1 not only restricts that a sender’s failure will cause a receiver’s failure, but also restricts that when the system is initialized, only the eventsnd_failure may occur. If we putrcv_failure before the eventsnd_failure in LTS Flow1, this LTS will violate the flow requirement. We get the system-level LTS of Level1 as shown in Figure 8, and its FSP expression is∥Sys1 =(S1∥R1∥Flow1∥Flow2).Figure 8
The system LTS of first refinement.We map the LTS models of Level1 to the iUML-B state machine and get the four state machines as shown in Figure9, whereSNDMachine1 andRCVMachine1 are the component state machines of the sender and receiver, respectively, and Flow1 and Flow2 correspond to LTS Flow1 and LTS Flow2, respectively.Figure 9
iUML-B state machines of first refinement.
(a)
SNDMachine1 (b)
RCVMachine1 (c)
Flow1 state machine (d)
Flow2 state machineSecond Refinement. The second level refinement only introduces one eventrcv_current_data, which does not involve the flow requirement associated with the sender, so we do not need to modify the sender component but only need to add eventrcv_current_data to the receiver’s component LTS, as Figure 10(b) shows. The FSP code isconst N = 2range T = 0⋯NR2=R2[0],R2 [r: T] = (when (r + 1 <N) rcv_current_data [r] -> R2 [r + 1]∣when (r + 1 == N) rcv_success->Rsucc∣rcv_failure->Rfail),Rsucc = (brp-> END),Rfail = (brp-> END).Figure 10
The iUML-B state machine RCVMachine2 and LTS R2.
(a)
RCVMachine2 (b)
LTS R2In the above codes, we introduce the message counterr of the receiver which represents the number of messages currently received. The constant N represents the total number of messages.We map Level2’s LTS model to the iUML-B state machine and get the new receiver state machine as shown in Figure10(a).In addition, we find thatr is a newly introduced variable, so we must model its changes using a new atomic LTS. We introduce a new atomic LTS RCV_QUEUE to express the change of r:RCV_QUEUE = RCV_QUEUE [0][0],RCV_QUEUE [s:T][r:T] = (when (r+1<N) rcv_current_data ->RCV_QUEUE [s][r+1]∣when (r+1==N)rcv_success-> RCV_QUEUE [s][r+1]).The LTS and the corresponding iUML-B state machine ofRCV_QUEUE are shown in Figure 11.Figure 11
The LTS and the corresponding iUML-B state machine ofRCV_QUEUE.
(a)
Rcv_queue state machine (b)
LTS Rcv_queueThis system-level LTS of level2 is shown in Figure12; the FSP expression is∥Sys2 =(S2 ∥R2 ∥Flow1 ∥Flow2 ∥RCV_QUEUE),Figure 12
The system LTS of second refinement.whereS2 =S1.At this level of refinement, there are no changes in the sender’s LTS and control flow LTS, so we do not need to modify the corresponding iUML-B state machine.Due to space limitations, we omitted the description of LTS model and iUML-B state machine model of the third layer refinement.


## 3.3. Property Verification of the Event-B Model

We use the iUML-B state machine to generate the BRP protocol control flow model in Event-B. These automatically generated control flow models have covered all the control variables of the fourth layer of Abiral’s BRP model. Thanks for iUML-B, we can refine the original component state machine and the flow state machine by adding new substates in the original state in the refinement of each layer and preserve the consistency of the Event-B model by refinement checks to ensure that concrete machine is the effective refinement of abstract machine.As we proved in Section2.3, the Event-B model we constructed is bisimulation equivalent to the original LTS model. Therefore, we can verify the properties of the Event-B model by verifying the properties of the original LTS model. We formalized the requirements of the BRP system of Table 1 using linear temporal logic (LTL) formulate; some of them are shown in Table 2. In Table 2, the symbol “□”, “U”, and “◇” represent “always”, “until”, and “eventually” in linear temporal logic, respectively, while the symbols “→”, “¬” and “∧” represent “implication”, “negative”, and “conjunction” in proposition logic, respectively.Table 2
The LTL formulate of basic requirements.
Requirement number LTL formulate Com0.1, Com0.2, Flow0.2 □(¬brp U (snd_progress∧rcv_progress)) Flow1.2 □(snd_failure→◇rcv_failure) Flow1.3 □(rcv_success→◇snd_success)We verified these properties with the help of the LTSA tool and the results show that the behavior of our model meets the requirements in Table1.


## 4. Discussion

There are four types of variables in Event-B model: Boolean variables (such ass∈TRUE,FALSE), variables with a finite number of states (such as s∈s1,s2,…,sn), data variables such as a∈N or a∈Z), and collection-type variables (e.g., g⊆D). As we can see, it is very easy to model the first two kinds of control variables using LTS. For data variables whose state space is an infinite set, we can use the following methods to model its changes: first, we bound the range of variablea using its lower bound and upper bound. That is, let a ∈ [lower bound, upper bound]; second, we divide the state space ofa into three subsets according to the equivalence class: a=lower  bound, lower  bound<a<upper  bound, and a=upper  bound. In this way, we can convert the infinite state space of data variable into a finite number of states and further establish the LTS model of this data variable. In fact, we have used this approach when we modeled Rcv_queue changes in the second level of refinement. However, the above method only works when we already know the range of data variable (such as the BRP model in this paper). For those data variables that we cannot determine their boundary, we need further research to model them. In addition, we still have not found an effective way to model changes of collection-type variables.


## 5. Related Work

There has been some research on explicitly simulating the control flow of the Event-B model. Fathabadi et al. [11] proposed a method named “Event Refinement Structure” (ERS) method which uses a tree structure based on the Jackson structure diagram (JSD) to express the control flow of Event-B model. However, one cannot establish the equivalence relationship between the tree structure of ERS and LTS. Therefore, it is also impossible to verify the behavioral properties of the ERS method. In contrast, our work uses the LTS and iUML-B state machine to visually express the control flow of the Event-B model and can verify its behavioral properties easily. Iliasov [12] proposed a method named flow language which usesena,dis, andfis to express the order of the events. However, the modeling elements of the flow method are the events and the relationships between events, rather than states and transitions of the state transition system. This makes flow language difficult to map onto LTS semantic model. Compared with the flow method, the iUML-B state machine uses the state-based style to express the control flow. This makes the control flow easier for engineers to understand.The combination of CSP and Classic B is also studied in [13, 14]. For the explicit control flow modeling of the Event-B, CSP∥B method [15] proposed an integrated formal method that combines Event-B as a state-based formal system and CSP as a control-based formal system to model the control flow in Event-B. Our approach is inspired by the CSP∥B method, but we use FSP to model the control flow of Event-B. Compared to the CSP∥B method, we systematically consider all the control variables that may affect the control flow of the Event-B machine. This makes our results of behavioral properties verification more reliable than CSP∥B. We compare our method (named “LTS+iUML-B”) with other methods in this field, as shown in Table 3.Table 3
Comparison of major control flow modeling methods.
Method Ability Formal behavior semantics Way of expression Convertible to LTS ERS No Tree structure No  Flow Method No Events and relationships No  CSP∥B Yes Process algebra Yes  LTS+iUML-B Yes States and transitions Yes


## 6. Conclusion

The Event-B model has some flaw in expressing the model’s control flow. In this paper, we use LTS to express Event-B control flow, which makes the control flow of Event-B model become visible and makes the verification of Event-B model’s behavior properties easier. We model each variable in the Event-B model that affects the model execution process as a single “atomic LTS” and use the LTS composition operation to obtain the control flow model of the entire system. By using our method, the modeler can easily observe and analyze the behavior of the system with the help of the LTSA tool. At the same time, we map the LTS model onto the Event-B model and prove the bisimulation equivalence between the original LTS model and the corresponding Event-B model. In this way, the modeler can verify the behavior of the Event-B model by verifying the properties of the original LTS model.At present, our modeling method is only suitable for Event-B’s Boolean variables, bounded state variables, and certain data variables. In the future, we will study how to use LTS to model the change of the collection-type variables in the Event-B model.



---

*Source: 8765186-2018-05-22.xml*