LTS Semantics Model of Event-B Synchronization Control Flow Design Patterns

1. Introduction

Event-B [1] is a formal language that is closest to software engineering. Its ideas of progressive refinement and ability of automatic code generation not only ensure the correctness and consistency of the model but also ensure the correctness of the final code. In order to enhance the reusability of the Event-B model to better support the software development process, the researchers proposed the Event-B design pattern [2], that is, the reusable Event-B models. The Event-B design pattern is similar to design pattern in software engineering but extends reusability to the correctness of the model, that is to say, the Event-B design patterns which have been verified can be instantiated as a part of the larger software model and do not need to be constructed it again and prove its correctness again. Now, the Event-B design pattern has been applied to embedded control systems [1], service-oriented architecture [3], software product line engineering [4,5], wireless sensor networks [6], and many other fields.

However, as a data-oriented modeling language, Event-B focuses only on the consistency of refinement, while it has limitations in the preservation and verification of behavioral properties. This is mainly because Event-B has no behavior semantics, which makes it difficult for the modeler to analyze and verify the linear temporal logic (LTL) behavior properties of the Event-B model directly. But it is well known that we should do more stringent verification on those components that will be more likely to be reused. Unfortunately, although the Event-B design pattern has been widely used, there is little research on its behavior semantics and verification of its behavioral properties.

In this paper, we propose a method to model the Event-B synchronize control design patterns using the labeled transition system (LTS). In detail, the contributions of this work are as follows.

We analyzed in detail the event order of the four Event-B synchronous control flow patterns, and revealed the complexity of the Event-B control flow design patterns as well as the difficulty to characterize it.

We proposed the concept of “atomic LTS” and used this concept to model the four synchronous control flow patterns. We proposed three transformation rules to construct “atomic LTS” and used rigorous logic derivation to prove the correctness of our transformation rules.

We constructed an LTS model of a complex multi-level control system using the LTS semantic model of the Event-B synchronous control flow design patterns. Our approach is to map the instantiation process of the Event-B model to the instantiation process of its corresponding LTS semantic model, which guarantees the behavioral equivalence between the source model (i.e., the Event-B model) and the target model (that is, the LTS semantic model).

We characterized the functional requirements and safety requirements of the complex multi-level control system using the LTL formula, and test these LTL behavioral properties of the target model using model checking tools to evaluate the feasibility of our method.

The rest of this paper is organized as follows: Section 2 discusses some related work and their flaws. In Section 3, we explain the principle of the Event-B synchronous control flow design pattern. Section 4 proposes three translation rules and gives the LTS behavior semantic model of the Event-B synchronous control pattern. Section 5 proposes the method to map the design pattern instantiation process of Event-B model to the instantiation process of LTS model and builds a complex control system model using this method. Section 6 gives the experimental results and discusses it. Section 7 concludes our work.

2. Related Work and Problem Definition

Event-B design pattern: Event-B design pattern is a reusable formal model that is different from the design pattern in the software engineering. The idea of the Event-B design pattern is to construct and prove the formal models of the relatively small problems in order to reuse these small formal models to construct the larger model. In this way, the modeler does not have to prove the correctness of these small models again. In other words, by using the Event-B design pattern, we can reuse not only the design strategy of the model but also the correctness of the model. Therefore, the direct benefit of the Event-B design pattern is that it can greatly reduce proof cost of the formal model.

Many Event-B design patterns have been proposed in recent years. For example, Silva and his colleague [7,8] proposed the Event-B design pattern and the “Generic Instantiation” approach and developed the Event-B model of the safety critical subway system. Yeganefard et al. [9] proposed the “MCMC” design patterns of Event-B model to model the generic formal components of the monitored, controlled, mode and commanded (MCMC) architecture. MCMC design patterns have been used to construct the Event-B model of cruise control system [10], automotive lane departure warning system [11], and lane centering controller [12]. The MCMC design pattern reuses the static architecture of the model, allowing the modeler to use this architecture directly when solving similar problems.

Modeling control flow of Event-B: How to characterize the control flow (i.e., event order)of Event-B code clearly, has always been a concern of researchers because it enables researchers to model and analyze the system’s behavior and further verify its behavioral properties (such as LTL properties). Fathabadi et al. [13,15] proposed a method named “atomic decomposition” which used a tree structure based on the Jackson structure diagram (JSD) to express the relationship between the abstract event and the subsequent concrete events as well as the order of concrete events. This method is used to construct the Event-B model of the multimedia protocol system [15] and the Space Craft system [16]. Iliasov [17] proposed a method named Flow language which uses ena, dis, and fis to express the order of the events, and uses the Flow plug-in to provide graphical symbols to model the event orders. Schneider et al. [18-20] proposed the CSP||B method, using communication sequential process (CSP) to express the control flow part of system, and using pure Event-B model to express the data processing part of system (that is, the computation part). Finally, he transforms the CSP model into the Event-B code and combines it with the computation part to form a complete Event-B model. We can verify the behavior of final Event-B model through verifying the behavior of CSP model. The inventor of Event-B, Abrial [1] proposed four synchronous control flow patterns, including strong synchronization pattern, weak synchronization pattern, strong-weak synchronization pattern, and strong-strong synchronization pattern. Its main purpose is to express the basic sub-problem in the reactive system, that is, the “trigger-response” relationship between components. We can use these patterns to establish the Event-B model of complex control system easily.

The LTL property of Event-B model: As we mentioned, one of the goals of modeling the control flow of Event-B code is to verify its behavioral properties. Literature in this area is rare. Current research is limited to how to preserve its LTL attributes during the refinement process of the Event-B model. For example, Schneider et al. [21] proposed a set of refinement strategies that can preserve the safety properties of Event-B models in the refinement chain. Further, Schneider et al. [22] extends this idea to the preservation of liveness properties and derives the refinement strategy that can preserve the temporal logic properties of the Event-B model throughout the refinement chain. Recently, Hoang et al. [23] gave more general results, which relax the constraints between adjacent refinement levels of Event-B model while ensuring that the LTL properties continue to hold during the refinement process.

2.1 Problems of Existing Research

Although many works have been done on the modeling of Event-B control flow and the LTL properties of Event-B, there are still some problems in current research.

First, these works cannot express Event-B’s control flow explicitly. Although the “atomic decomposition” method claims that it can express the control flow of Event-B, the control flow is not visible in its tree structure. Flow method uses the relationship between events to express control flow, which is contrary to the style of the traditional transition system. [TeX:] $$\mathrm{CSP} \| \mathrm{B}$$ method works best in this respect but still cannot express the control flow of a complete Event-B model. The synchronous control flow design pattern itself is expressed using Event-B code. The flaws in these methods make it impossible for people to clearly observe and analyze the behavior of the model.

Second, the results of these works are difficult to translate directly into LTS models. LTS is a traditional and authoritative behavioral semantic model, which is also the theoretical basis of LTL model checking. However, the results of various Event-B control flow modeling methods, such as atomic decomposition and Flow methods, cannot be directly converted to LTS models. Although the CSP has formal behavioral semantics and can be directly mapped to the LTS model, the CSP||B method only expresses a part (that is, the control flow) of the Event-B model using the CSP. Therefore, using\ [TeX:] $$\mathrm{CSP} \| \mathrm{B}$$, we cannot get a complete LTS model of Event-B model.

Finally, these works do not support verification of the LTL property of the Event-B model. Although Schneider et al. [21,22] and Hoang et al. [23] studied the behavioral semantics and LTL properties preservation of Event-B, their constraints on the refinement strategy of the Event-B model will limit the exploration of the design space for the Event-B model.

In conclusion, the available control flow modeling methods have some limitations and do not support verification of LTL properties. In contrast, we propose an explicit way to model Event-B control flow and give its LTS behavioral semantics that can support LTL properties verification.

3. Event-B Synchronous Control Flow Design Patterns

Event-B is an event-based formal modeling language whose core concept is event. The general form of an event is as follows:

An event is made up of guards and actions. An event e is enabled when its guards are satisfied, and actions express the effect of the event e, that is, the modification of the variables. Event-B uses variables to express the state of the system and perform the state changes with events.

Abrial [1] proposed four synchronous control flow patterns to abstract the basic “trigger-response” relationship in a multi-level control system. The basic principle of “trigger-response” relationship is shown in Fig. 1.

In Fig. 1, the actuator executes the action event, and modifies its own state. The reactor is enabled after the action event and can execute the reaction event.

In the synchronous control flow design pattern, the variables a, b and r, s are used to represent the state of the actuator and the reactor, respectively. The x_on event changes the value of the variable x from 0 to 1, and the event x_off changes the value of the variable x from 1 to 0, where [TeX:] $$x \in\{a, r, b, s\}$$ We refer to a pair of “actuators – reactors” as a “subsystem”.

For the sake of discussion, we first consider an Event-B model including the actuator a and reactor r with no synchronization control relationship, named non_control_model:

In non_control_model, there is no r-related expression in the guards of the a_on and a_off events. Thus, the occurrence of the above two events is not constrained by the variable r. Likewise, the r_on and r_off events are not constrained by the variable a.

3.1 Weak Synchronization Pattern

The weak synchronization pattern means that after the actuator executes trigger event a_on, the reactor can either respond to it (execute the r_on event) or make no response (do not execute the r_on event). This relationship also applies to events a_off and r_off. A realistic case of this pattern is the response of the keyboard to the keystroke event—in many cases, a user may trigger many “button is pressed” events in one second because of his finger jitter, but in fact, he just wants to trigger one event.

The principle of weak synchronization pattern is shown in Fig. 2. Where the two signals labeled by a and r represent the states of the actuator a and the reactor r, respectively. The rising edge indicates that the value of a or r changes from 0 to 1 while the falling edge changes their values from 1 to 0.

The Event-B model of the weak synchronization pattern, weak_model is:

Compared with the non_control_model, weak_model adds some constraint in the event r_on and r_off, which specifies that the r_on event can occur only when a = 1 (event a_on has occurred). Similarly, r_off events can only occur after event a_off. We added some dashed arrows to the Event-B model to indicate the triggering relationship between events. They indicate that two events will be enabled, a_off and r_on after the a_on event occurs. Similarly, after the action1: a:= 0 in the a_off event is performed, there are two events be enabled, a_on and r_off.

3.2 Strong Synchronization Pattern

The strong synchronization pattern is similar to the synchronous call in the function call, that is, the reactor r must perform the event r_on after the actuator a executes the event a_on, otherwise the actuator will wait forever until the reactor responds. Thus, the actuator can only execute the a_off event after the reactor executes the r_on event, and the reactor must, in turn, execute the r_off event after a_off event occurs. The principle of strong synchronization pattern is shown in Fig. 3.

The Event-B model of the strong synchronization pattern, strong_model is:

Strong_model adds more constraints to the actuator events a_on and a_off of the weak_model so that the events in the model must only be executed in the order indicated by the dashed arrows.

3.3 Strong-Weak Synchronization Pattern

In a multi-level control system, there is also a “trigger-response” relationship between subsystems. For example, if we name the strong synchronization subsystem composed of the actuator a and the reactor r as sub-system 1, while name the strong synchronization subsystem composed of the actuator b and the reactor s as sub-system 2, then the strong-weak synchronization relation describes the “weak triggerresponse” relationship between these two strong synchronization subsystems. The principle of strongweak synchronization is shown in Fig. 4.

In a multi-level control system, there is also a “trigger-response” relationship between subsystems. For example, if we name the strong synchronization subsystem composed of the actuator a and the reactor r as sub-system 1, while name the strong synchronization subsystem composed of the actuator b and the reactor s as sub-system 2, then the strong-weak synchronization relation describes the “weak triggerresponse” relationship between these two strong synchronization subsystems. The principle of strongweak synchronization is shown in Fig. 4.

The Event-B model of the strong-weak synchronization pattern, strong_weak_model is:

Although we use the dotted arrows to express as clearly as possible the order of events in the strongweak synchronization relationship, it is obvious that it is very difficult to clearly analyze the event order in such a two-level control system model. For the more complex multi-levels control system, it is almost impossible to intuitively and clearly express the event order of system model.

3.4 Strong-Strong Synchronization Pattern

The strong-strong synchronization pattern means that: firstly, the reactor r of the subsystem 1 is the trigger of the actuator b of the subsystem 2. The subsystem 2 must perform the b_on event as long as the r_on event occurs. Secondly, once the b_on event occurs, then the subsequent event must be s_on, b_off, s_off because the subsystem 2 is a strong synchronization system. Thirdly, the subsystem 1 will maintain its state (that is, a = 1, r = 1) after r_on event occurs until the s_off event is executed by the subsystem 2. That is to say, the a_off event must be triggered by the s_off event. The principle of strong- strong synchronization is shown in Fig. 5.

The Event-B model of the strong-weak synchronization pattern, strong_strong_model is:

In the strong_strong_model, a state variable m has been added based on strong_weak_model to constrain the relationship between a_on and a_off, which means a_off can be executed only after the b_on event occurs. Since b and s composed a strong synchronization subsystem, when b_on occurs, it means that its subsequent events must be s_on, b_off and s_off, so a_off only can occur after the event sequence “b_on, s_on, b_off, s_off”, that is, a_off only can occur after the s_off event.

We can see that: firstly, the event order of Event-B design patterns is difficult to analyze. Secondly, the process from the non_control_model to the weak_model and then to the strong_model is an incremental process that enhances the constraint. Similarly, from the strong_weak_model to strong_strong_model is also an increasing constraint enhancement process. This inspires us to establish the LTS semantic models of the four synchronic control flow patterns in an incremental way.

4. The LTS Model of the Event-B Synchronization Patterns

In this section, we will build the LTS behavior semantic model of the Event-B synchronous control flow design pattern. LTS is a state transition system in which the transition is labeled as an action. The action set of the LTS is called its communication alphabet.

Definition 1.1 (LTS [24]): Let States represent a universal set of states, Acts represents a universal action set, and then an LTS P is defined as a quaternion [TeX:] $$P=<Q, \Sigma, \Delta, q>$$ where:

[TeX:] $$Q \subseteq$$States, representing the state set of P;

[TeX:] $$\Sigma=\alpha P(\alpha P \subseteq A c t s)$$, representing the action set of P;

[TeX:] $$\Delta \subseteq Q \times \Sigma \times Q$$, representing the transition relationship in P, these transitions are labeled with the elements in ;

[TeX:] $$q \in Q$$, representing the initial state of P.

An LTS P can be converted to LTS P' by action [TeX:] $$a \in A$$, denoted [TeX:] $$P \stackrel{a}{\rightarrow} P^{\prime}, \text { if } P^{\prime}=<Q, \Sigma, \Delta, q^{\prime}>$$ and (q, a, q′)[TeX:] $$\in \Delta$$

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 1.2 Parallel composition of LTSs: The parallel composition of two LTS [TeX:] $$M=<Q_{1}, \Sigma_{1}, \Delta_{l}, q_{1}>$$ and [TeX:] $$N=<Q_{2}, \Sigma_{2}, \Delta_{2}, q_{2}>$$ are expressed as [TeX:] $$\operatorname{LTS}(M \| N)=<Q_{1} \times Q_{2}, \Sigma_{1} \cup \Sigma_{2}, \Delta,\left(q_{1}, q_{2}\right)>$$, where is the minimum relation that satisfies the following constraint:

where [TeX:] $$a \in \Sigma_{1} \cup \Sigma_{2}, \tau$$, represents an internal action that is not visible to the outside.

We start from the LTS model of the basic non_control_model, and gradually construct the LTS model of the four synchronization patterns.

Our basic idea is to treat an Event-B model as a composite LTS while treating each state variable of this Event-B model as an atomic LTS. Therefore, the LTS of Event-B model is the parallel composition of all atomic LTSs. The advantage of this idea is that, although the LTS model of an Event-B model is very complex, we can break it into some little atomic LTSs. Each atomic LTS corresponds to the state transition of a single variable which is easy to be modeled.

Our translation method is based on a basic fact in Event-B model, that is, the occurrence of an event will change the value of a variable. Thus, for each atomic LTS, we can mark the event that causes its state change to a transition edge in this LTS. The source node of this transition is the value of the variable before the event occurs, while the destination node is the value of the variable after the event occurs. In

this way, we get the following two translation rules:

Rule 1. Each variable in the Event-B model is modeled as an atomic LTS, and all possible values for this variable form the state space of this atomic LTS.

Rule 2. For each atomic LTS P, if an event e in the Event-B model changes the value of its corresponding variable from s1 to s₂, then we add an element [TeX:] $$\left(s_{1} \stackrel{e}{\rightarrow} s_{2}\right)$$ to the transition set of this atomic LTS.

4.1 LTS Model of non_control_model

According to Rules 1 and 2, we can easily get the LTS model of a_n and r_n in non_control_model, namely the LTS A_N and the LTS R_N :

[TeX:] $$LTS\ A_{N}=<\{0,1\},\left\{a_{-} o n, a_{-} o f f\right\}, \left\{\left(0 \stackrel{a_{-} o n}{\longrightarrow} 1\right),\left(1 \stackrel{a_{-} o f f}{\longrightarrow} 0\right)\right\}, 0>

[TeX:] LTS\ R_{N}=<\{0,1\},\left\{r_{-} o n, r_{-} o f f\right\},\left\{\left(0 \stackrel{r_{-} o n}{\longrightarrow} 1\right),\left(1 \stackrel{r_{-} o f f}{\longrightarrow} 0\right)\right\}, 0>$$

The LTS model of non_control_model is equal to the parallel composition of LTS A_N and LTS R_N， namely LTS N. According to the parallel composition rules in Definition 1.2, we get:

[TeX:] $$L T S\ N=L T S\left(A_{N} \| R_{N}\right)=<Q_{N}, \Sigma_{N}, \Delta_{N,} q_{N>},$$ where：

[TeX:] $$Q_{N}=\{(0,0),(0,1),(1,1),(1,0)\}$$

[TeX:] $$\Sigma_{N}=\left\{a_{-} \text { on, } a_{-} o f f, r_{-} \text { on, } r_{-} \text { off }\right\}$$

[TeX:] $$\Delta_{N}=\left\{(0,0) \stackrel{a_{-} o n}{\longrightarrow}(1,0),(0,1) \stackrel{a_{-} o n}{\longrightarrow}(1,1)\right.(1,1) \stackrel{a_{-} o f f}{\longrightarrow}(0,1),(1,0) \stackrel{a_{-} o f f}{\longrightarrow}(0,0)\\ (0,0) \stackrel{r_{-} o n}{\longrightarrow}(0,1),(1,0) \stackrel{r_{0}-o n}{\longrightarrow}(1,1),(0,1) \stackrel{r_{o f f}}{\longrightarrow}(0,0),(1,1) \stackrel{r_{o f f}}{\longrightarrow}(1,0) \} $$

[TeX:] $$q_{N}=(0,0)$$.

The state transition diagram for the atomic LTS of a_n and r_n as well as composed LTS N is shown in Fig. 6. The "" symbol in Fig. 6 is parallel composition operator.

4.2 LTS Model of weak_model

If there is no interaction between the atomic LTSs, that is, the change of one state variable in the Event- B model does not affect the change of another state variable, just like non_control_model, then the Rules 1 and 2 are sufficient to build the LTSs of Event-B model. But in the actual situation, this is usually not the case. Therefore, we also need to consider the impact of interaction in the Event-B model on the atomic LTSs.

In Section 3.1, we have already shown that the Event-B model of the weak synchronize pattern can be obtained by adding some guards to the non_control_model (e.g., add a guard “a = 1” for the r_on event of non_control_model). Now we need to map this change to the LTS of the actuator a and the reactor r.

However, there is currently no rule that can be applied to r_on because the r_on event does not change the value of a. Thus, we use a tricky approach to transform the r_on event into an r_on' event in which a “useless” action named action2: a ≔ 1 is added:

It is obvious that r_on and r_on' has the same behavior semantics. They all do the same behavior, “change the value of variable a from 1 to 1”. While this sounds ridiculous, it can help us to construct LTS through the code of r_on. Now, according to Rule 2, we can add a new transition [TeX:] $$\left(1 \stackrel{r_{-} O n}{\longrightarrow} 1\right)$$ to the transition set of atomic LTS of a. It should be noted that although guard1: a = 1 appears in the guards of r_on, it describes the impact of event r_on on variable a, so the LTS we need to modify is the LTS of a.

After generalization of the above situation, we can get Rule 3.

Rule 3. Assume that s is a variable in an Event-B model; q_i is a possible value for q. If there is an expression “q = q_i ” in the guards of event e, and the action of event e does not change the value of q, then we should add a transition [TeX:] $$\left(q_{i} \stackrel{e}{\rightarrow} q_{i}\right)$$ to the transition set of LTS of variable q.

Rule 3 is a special case of Rule 2. In the LTS transition graph, it means that a reflexive edge is added to the qi state node in the LTS of q, and the edge is labeled with event e.

Now, according to Rule 3 and weak_model, we can easily get the LTS model of a_w and r_w in weak synchronization pattern, namely LTS A_w and LTS R_w:

[TeX:] $$L T S\ A_{w}=<\{0,1\},\left\{a_{-} o n, a_{-} o f f, r_{-} o n, r_{-} o f\right\}, \left\{\left(0 \stackrel{a_{-} o n}{\longrightarrow} 1\right),\left(1 \stackrel{a_{-}o f f}{\longrightarrow} 0\right),\left(0 \stackrel{r_{-}o f f}{\longrightarrow} 0\right),\left(1 \stackrel{r_{-}o n}{\longrightarrow} 1\right)\right\}, 0>$$

[TeX:] $$\\ L T S\ R_{w}=<\{0,1\},\left\{r_{-} o n, r_{-} o f\right\}, \left\{\left(0 \stackrel{r_{-} o n}{\longrightarrow} 1\right),\left(1 \stackrel{r_{-} o f f}{\longrightarrow} 0\right)\right\}, 0> $$

The LTS model of weak _model is equal to the parallel composition of LTS AW and LTS AW, namely LTS W:

[TeX:] $$L T S\ W=L T S\left(A_{w} \| R_{w}\right)=<Q_{W}, \Sigma_{W}, \Delta w, q_{w}>,$$, where:

[TeX:] $$Q_{W}=\{(0,0),(0,1),(1,1),(1,0)\}$$

[TeX:] $$\Sigma_{W}=\left\{a_{-} o n, a_{-} o f f, r_{-} o n, r_{-} o f f\right\}$$

[TeX:] $$\Delta_{W}=\left\{(0,0) \stackrel{a_{-} o n}{\longrightarrow}(1,0),(0,1) \stackrel{a_{-} o n}{\longrightarrow}(1,1)\right.,(1,1) \stackrel{a_{-} o f f}{\longrightarrow}(0,1),(1,0) \stackrel{a_{-} o f f}{\longrightarrow}(0,0),(1,0) \stackrel{r_{-}o n}{\longrightarrow}(1,1),(0,1) \stackrel{r_{-} o f f}{\longrightarrow}(0,0) \}$$

[TeX:] $$q_{\mathrm{W}=(0,0)}.$$

The state transition diagram for the atomic LTS of a_w and r_w as well as composed LTS W is shown in Fig. 7.

We can see that the LTS of the weak synchronization pattern is in fact a clipping of the LTS N. Compared to the transition set _N, there are two transitions [TeX:] $$\left(0,0) \stackrel{r_{-}o n}{\longrightarrow}(0,1)\right.\ and\ (1,1) \stackrel{r_{-} o f f}{\longrightarrow}(1,0))$$ removed from the transition set _w, which is the effect of adding guards on events r_on and r_off.

4.3 LTS Model of strong_model

According to Rule 3 and strong_model, we continue to construct LTS models of a_s and r_s in strong synchronization patterns, named LTS A_s and LTS R_s:

[TeX:] $$L T S\ A s=<\{0,1\},\ \left\{a_{-} o n, a_{-} o f f, r_{-} o n, r_{-} o f f\right\},\left\{\left(0 \stackrel{a_{-}o n}{\longrightarrow} 1\right)\right. ,\left(1 \stackrel{a_{-} \circ f f}{\longrightarrow} 0\right),\left(0 \stackrel{r_{0} f f}{\longrightarrow} 0\right),\left(1 \stackrel{r_{0} n}{\longrightarrow} 1\right) \}, 0>$$

[TeX:] $$L T S\ R_{S}=<\{0,1\},\left\{a_{-} O n, a_{-} O f f, r_{-} O n, r_{-} O f f\right\},\left\{\left(0 \stackrel{r_{-}o n}{\longrightarrow} 1\right),\left(1 \stackrel{r_{-} o f f}{\longrightarrow} 0\right)\right.,\left(0 \stackrel{a_{-} o n}{\longrightarrow} 0\right),\left(1 \stackrel{a_{-} o f f}{\longrightarrow} 1\right) \}, 0> $$

The LTS model of strong _model is equal to the parallel composition of LTS A_s and LTS R_s，namely LTS S:

[TeX:] $$L T S\ S=L T S\left(A_{S} \| R_{S}\right) =<Q_{S}, \Sigma_{S}, \Delta_{S}, q_{S}>,$$,where：

[TeX:] $$Q s=\{(0,0),(0,1),(1,1),(1,0)\}$$

[TeX:] $$\Sigma_{S}=\left\{a_{-} o n, a_{-} o f f, r_{-} o n, r_{-} o f f\}\right.$$

[TeX:] $$\Delta_{S}=\left\{(0,0) \stackrel{a_{-} o n}{\longrightarrow}(1,0)\right.,(1,0) \stackrel{r_{-} o n}{\longrightarrow}(1,1)(1,1) \stackrel{a_{-} o f f}{\longrightarrow}(0,1),(0,1) \stackrel{r_{-} o f f}{\longrightarrow}(0,0) \}$$

[TeX:] $$q_{S}=(0,0)$$

The state transition diagram for the atomic LTS of a_s and r_s as well as composed LTS S is shown in Fig. 8.

4.4 LTS Model of strong_weak_model

Strong_weak_model seems to be the most complex, but in fact, we can easily get LTS models of each variable according to the Rules 1 to 3. First, according to Rulex 1 and 2, we establish the atomic LTS models of a_sw, r_sw, b_sw and s_sw respectively. Then we add the synchronization control transitions on these atomic LTSs according to Rule 3 and strong_weak_model. The final atomic LTS models are:

[TeX:] $$L T S\ A s w=<\{0,1\},\left\{a_{-} o n, a_{-} o f f, r_{-} o n, r_{-} o f f, b_{-} o n\right\},\left\{\left(0 \stackrel{a_{-} \circ n}{\longrightarrow} 1\right),\left(1 \stackrel{a_{-}of f}{\longrightarrow} 0\right)\right.,\left(0 \stackrel{r_{-}o f f}{\longrightarrow} 0\right),\left(1 \stackrel{r_{-}o n}{\longrightarrow} 1\right),\left(1 \stackrel{b_{-}o n}{\longrightarrow} 1\right) \}, 0>$$

[TeX:] $$L T S\ R_{S W}=<\{0,1\},\left\{a_{-} o n, a_{-} o f f, r_{-} o n, r_{-} o f f, b_{-} o n\right\},\left\{\left(0 \stackrel{r_{-} \circ n}{\longrightarrow} 1\right),\left(1 \stackrel{r_{-} \circ f f}{\longrightarrow} 0\right)\right.,\left(0 \stackrel{a_{-} o n}{\longrightarrow} 0\right),\left(1 \stackrel{a_{-} o f f}{\longrightarrow} 1\right),\left(1 \stackrel{b_{-} o n}{\longrightarrow} 1\right) \}, 0>$$

[TeX:] $$L T S\ B_{S W}=<\{0,1\},\left\{b_{-} o n, b_{-} o f f, s_{-} o n, s_{-} o f f, a_{-} o f f\right\},\\ \left\{\left(0 \stackrel{b_{\longrightarrow} \circ n}{\longrightarrow} 1\right)\right.,\left(1 \stackrel{b_{-} o f f}{\longrightarrow} 0\right),\left(0 \stackrel{a_{-} \mathrm{off}}{\longrightarrow} 0\right),\left(0 \stackrel{s_{-o f f}}{\longrightarrow} 0\right),\left(1 \stackrel{s_{-}o n}{\longrightarrow} 1\right) \}, 0>$$

[TeX:] $$L T S\ S_{S W}=<\{0,1\},\left\{b_{-} o n, b_{-} o f f, s_{-} o n, s_{-} o f f, a_{-} o f f\right\},\\ \left\{\left(0 \stackrel{s_{-} o n}{\longrightarrow} 1\right),\left(1 \stackrel{s_{-} o f f}{\longrightarrow} 0\right)\right.,\left(0 \stackrel{b_{-} o n}{\longrightarrow} 0\right),\left(0 \stackrel{a_{-} o f f}{\longrightarrow} 0\right),\left(1 \stackrel{b_{-} o f f}{\longrightarrow} 1\right) \}, 0>$$

The LTS model of strong_weak_model is equal to the parallel composition of these four LTSs, namely LTS SW:

[TeX:] $$L T S\ S W=L T S\left(A_{s W}\left\|R_{S W}\right\| B_{S W} \| S_{S W}\right)=<Q_{S W}, \sum_{S W}, \Delta_{S W}, q_{S W}>$$,where：

[TeX:] $$Q_{s w}=\{(0,0,0,0),(0,1,0,0),(1,1,0,0),(1,0,0,0),(1,1,0,1),(1,1,1,1),(1,1,1,0) \}$$

[TeX:] $$\Sigma_{S W}=\left\{a_{-} o n, a_{-} o f f, r_{-} o n, r_{-} o f f, b_{-} o n, b_{-} o f f, s_{-} o n, s_{-} o f f\right\}$$

[TeX:] $$\Delta_{S W}=\left\{(0,0,0,0) \stackrel{a_{-}o n}{\longrightarrow}(1,0,0,0)\right.,(1,0,0,0) \stackrel{r_{-}o n}{\longrightarrow}(1,1,0,0),(1,1,0,0) \stackrel{a_{-}o f f}{\longrightarrow}(0,1,0,0),\stackrel{r_{-} o f f}{\longrightarrow}(0,0,0,0), \\ (1,1,0,0) \stackrel{b_{-} o n}{\longrightarrow}(1,1,1,0),(1,1,1,0) \stackrel{s_{-} o n}{\longrightarrow}(1,1,1,1),(1,1,1,1) \stackrel{b_{-} o f f}{\longrightarrow}(1,1,0,1),(1,1,0,1) \stackrel{s_{-}o f f}{\longrightarrow}(1,0,0,0) \} $$

[TeX:] $$q s W=(0,0,0,0)$$

The state transition diagram for the atomic LTS of a_sw, r_sw, b_sw, s_sw as well as composed LTS SW is shown in Fig. 9.

4.5 LTS Model of strong_ strong_model

In Section 3.4, we already know that strong_strong_model is actually just adding some constraints on the basis of strong_weak_model (by adding a variable m to constrain the execution order of a_on, b_on and a_off). So we only need to add a new LTS M base on LTS SW to constrain it:

[TeX:] $$L T S\ A_{S S}=L T S\ A s w$$

[TeX:] $$L T S\ R_{S S}=L T S\ R_{S W}$$

[TeX:] $$L T S\ B_{S S}=L T S\ B_{S W}$$

[TeX:] $$L T S\ S_{S S}=L T S\ S_{S W}$$

[TeX:] $$L T S\ M=<\{0,1\},\left\{a_{-} o n, b_{-} o n, a_{-} o f f\}\right.,\left\{\left(0 \stackrel{a_{-} \circ n}{\longrightarrow} 1\right),\left(1 \stackrel{b_{-} \circ n}{\longrightarrow} 0\right)\right.,\left(0 \stackrel{a_{-}o f f}{\longrightarrow} 0\right) \}, 0>$$

The state transition diagram for LTS M is shown in Fig. 10.

The LTS model of strong_strong _model is equal to the parallel composition of LTS A_ss, LTS R_ss, LTS B_ss, LTS S_ss, and LTS M, namely LTS SS:

[TeX:] $$L T S\ S S=L T S\left(A_{s s}\left\|R_{s s}\right\| B_{s s}\left\|S_{s s}\right\| M\right)=<Q_{s s}, \Sigma_{s s}, \Delta_{s s}, q_{s s}>,$$where：

[TeX:] $$Q_{s s}=\{(0,0,0,0,0),(0,1,0,0,0),(1,1,0,0,0),(1,1,0,1,0),(1,1,1,1,0),(1,1,1,0,0),(1,1,0,0,1),(1,0,0,0,1) \}$$

[TeX:] $$\Sigma_{S S}=\left\{a_{-} o n, a_{-} o f f, r_{-} o n, r_{-} o f f, b_{-} o n, b_{-} o f f, s_{-} o n, s_{-} o f f\right\}$$

[TeX:] $$\Delta_{s s}=\left\{(0,0,0,0,0) \stackrel{a_{-}o n}{\longrightarrow}(1,0,0,0,1),(1,0,0,0,1)\right.,\stackrel{r_{-}0 n}{\longrightarrow}(1,1,0,0,1),(1,1,0,0,1) \stackrel{b_{-}o n}{\longrightarrow}(1,1,1,0,0), \\(1,1,1,0,0) \stackrel{s_ {-}o n}{\longrightarrow}(1,1,1,1,0),(1,1,1,1,0) \stackrel{b_{-}o f f}{\longrightarrow}(1,1,0,1,0),(1,1,0,1,0) \stackrel{s_{-} off}{\longrightarrow}(1,1,0,0,0), \\(1,1,0,0,0) \stackrel{a_{-} o f f}{\longrightarrow}(0,1,0,0,0),(0,1,0,0,0) \stackrel{r_{-} o f f}{\longrightarrow}(0,0,0,0,0) \}$$

[TeX:] $$q_{S S}=(0,0,0,0,0)$$

5. Case Study

In this section, we apply the LTS semantic model of the four synchronous control flow design patterns of Event-B to the behavior model construction of a complex multi-level control system. We map the instantiation process of the Event-B model to the instantiation process of its corresponding LTS semantic model, and obtain the LTS semantic model of the Event-B model of the complex control system. On this basis, we use LTL to describe the behavior properties of the Event-B model and verify them. In this way, we can verify the behavioral properties of each refinement level of the Event-B model until the final refinement model is verified. Since the Rodin platform (an Event-B modeling environment) provides a mechanism for refinement checking, we do not need to be concerned with the correctness of refinement, but only to verify the behavioral properties of each LTS model.

The modeling and verification processes are shown in Fig. 12. The leftmost part of the Fig. 12 is a common process to get the Event-B model of a complex control system by the instantiations of Event-B design patterns. The middle of Fig. 12 is the process of enhancing the constraints of the LTS according to the refinement process of the Event-B model. The rightmost part of Fig. 12 is the property verification process of the LTS model corresponding to the Event-B model. We guarantee that at each refinement level, there are [TeX:] $$M_{i} \Leftrightarrow L_{i}$$, and then verify the LTL properties of the LTS model, i.e. [TeX:] $$L_{i} \vDash P_{i}$$. In this way, we can guarantee [TeX:] $$M_{i} \vDash P_{i}$$. The formula at the bottom of Fig. 12 is a formal representation of this conversion and verification process.

5.1 System Description

We use the complex control system design patterns in the study of Abrial [1] to illustrate our approach. The system is called the mechanical press control system. The system has four control buttons, which include two motor control buttons and two clutch control buttons to start and stop the system components. After the motor is started, if the clutch is engaged, the rod will drive the slide up and down to use the tool to process the part. A door is used to prevent the worker from putting his hand under the tool while processing the part. The physical composition of the system is shown in Fig. 13(a).

The complete internal composition of the system and the synchronization control relationship between the components are shown in Fig. 13(b).We use the dotted line shadow box to represent the subsystem. For example, there is a “trigger-response” relationship between the “start motor button” and the “controller”, so we put them into a subsystem, that is, Sub1. At the same time, we use the dotted arrows to express the “trigger-response” relationship between the components or subsystems. The starting point of the arrow indicates the actuator component or the actuator subsystem, and the end point of the arrow represents the reactor part or the reactor subsystem. For example, the arrow with the “start motor button” as the starting point and the “controller” as the end point indicate that in the subsystem 1, the “start motor button” is the actuator and the “controller” is the reactor. We marked the type of synchronization relationship on the arrow. For example, the relationship between Sub5 and Sub7 is a strong - weak synchronization relationship.

Abrial [1] used the instantiation methods to progressively introduce the various subsystems and various synchronic control flow relationships into the model during the refinement process and ended this process at the seventh refinement layer. The shaded portion of Fig. 12 represents this refinement process. We need to complete the process shown in the middle part and the rightmost part of Fig. 12.

5.2 Instantiation Process of LTS Model

The instantiation process from the Event-B design pattern to the Event-B system model is a very simple renaming process, as we will see in Table 1. The principle behind this process is that modifying the variable name, constant name, and event name will not affect the correctness and refinement consistency of the system. We apply this idea to the LTS behavior semantic model of Event-B design pattern, and get the LTS model of Event-B system model by instantiating the LTS behavior semantic model of Event-B design pattern. The instantiation process of the LTS model is also very simple, that is, renaming the name of the state, conversion and atomic LTS of LTS behavior semantics model. It is obvious that the instantiation of the LTS behavior semantic model does not change the behavior of the LTS model itself, either.

We use an example of strong synchronization pattern to illustrate the correspondence between the process of instantiation of Event-B design pattern and the process of instantiation of the LTS behavior semantic model of Event-B design pattern.

The relationship between the controller and the motor in Sub5 in Fig. 13 are a strong synchronization relationship. Abrial [1] instantiates the Event-B design pattern strong_model in Section 3.2 into the Event- B model of Sub5, namely controller_motor_model. Corresponding to this process, we instantiate the atomic LTSs model of the strong synchronization pattern, that is LTS AS and LTS RS in Section 4.3, into their LTS model, namely Motor_actuator0 and Motor_sensor0, respectively, then perform the parallel composition operation on them to get the LTS behavior semantic model of controller_motor_model, named LTS Press0. The correspondence between these two processes is shown in Table 1. The instantiation process of Event-B design pattern is just to rename the elements of column 2 of Table 1 to the elements of column 3 of Table 1. Similarly, the instantiation process of LTS is just to rename the elements of column 5 of Table 1 to the elements of column 6 of Table 1.

The controller_motor_model of Sub5 obtained by instantiation of strong_model is:

The LTS behavior model of controller_motor_model is the parallel composition of the two LTSs in Fig. 14, that is, LTS Press0 shown in Fig. 15.

We use this method to convert each layer of the Event-B model of mechanical press control system into the corresponding LTS semantic model. In the last layer, that is, the seventh layer, we get 15 atomic LTSs, of which 14 are shown in Table 2. The LTS that not be shown in Table 2 is the LTS M in Section 4.5, which is used to model the strong-strong synchronization pattern.

The final system LTS model, named LTS Press7, is the parallel composition of the above 15 LTSs, that is:

[TeX:] $$LTS\ Press7=L T S\ S u b 1\|L T S\ S u b 2\| L T S\ S u b 3\|L T S\ S u b 4\|L T S\ S u b 5\|L T S\ S u b 6\| L T S\ S u b 7 \| L T S\ M ,where:$$

[TeX:] $$L T S\ S u b 1=start_{-} \text { motor }_{-} \text { button } \| \text {start}_{-}motor_{-}impulse;$$

[TeX:] $$L T S\ S u b 2=s t o p_{-} \text { motor }_{-} \text { button } \| \text {stop}_{-}motor_{-}impulse;$$

[TeX:] $$L T S\ S u b 3=start_{-} \text { clutch }_{-} \text { button } \| \text {start}_{-}clutch_{-}impulse;$$

[TeX:] $$L T S\ S u b 4=stop_{-} \text { clutch }_{-} \text { button } \| \text {stop}_{-}clutch_{-}impulse;$$

[TeX:] $$L T S\ S u b 5= \text { motor }_{-} \text { actuator } \| \text {motor}_{-}sensor$$

[TeX:] $$L T S\ S u b 6= \text {door }_{-} \text { actuator } \| \text {door}_{-}sensor$$

[TeX:] $$L T S\ S u b 7= \text {clutch }_{-} \text { actuator } \| \text {clutch}_{-}sensor$$

5.3 Verification of the Behavior Properties

Now we can complete the rightmost process in Fig. 12, that is, the behavior properties verification of the LTS model. Due to space limitations, we only give behavior properties verification process of the final model Press7. Abrial [1] specifies the basic requirements for the mechanical press control system, as shown in Table 3.

We write LTL expressions according to the requirements in Table 3, as shown in Table 4. The symbol “ ”and “U” in Table.4 represent “always” and “Until” in linear temporal logic, respectively, while the symbols “¬” and “→” represent “negation” and “implication” in proposition logic, respectively.

We verified the LTL behavior properties of LTS model of each refinement layer of the Event-B model and find that the system model at some intermediate layers does not satisfy the required behavior properties. But in the last layer, that is, the seventh layer, all of the behavioral properties are satisfied. This is because Event-B’s refinement strategy does not take into account the preservation of behavioral properties. It also suggests that our method is necessary.

6. Experimental Results and Discussion

In this section, we compare the results of our work with previous research in three aspects: explicit expression of control flow, model simulation and analysis capabilities, and support for LTL properties verification.

6.1 Comparison of Explicit Expression Ability of Control Flow

We show the LTS model of strong-weak synchronization pattern in Fig. 16. As can be seen from Fig. 16, while the event order of the Event-B design pattern given in Section 4 seems to be complicated, it is easier to observe the event order in its LTS model. Compared with the way of expression of LTS model, the CSP||B method uses the textual form of “Process P-> action. Process Q” to express the sequence of events. The advantage of this is that the code is concise, but also causes the order of its actions to be invisible; “atomic decomposition” method and Flow methods also use a graphical way to describe the relationships between events. However, the main advantage of the “atomic decomposition” method is to express the relationship between abstract and concrete events, not the event order. We must analyze its tree structure carefully to understand the actual control flow of Event-B model; The Flow method uses a

style like “event a enable/disable event b” to express the relationship between events, which does not conform to the traditional way of expression of control flow (i.e., the state transition system style).

6.2 Comparison of Model Simulation and Analysis Capabilities

We counted the relevant data of the Event-B model of the mechanical press control system, as shown in Table 5 and Fig. 17. At the same time, we presented the statistics of the LTS model of the mechanical press control system, as shown in Table 6 and Fig. 18. Since the LTS model is just the behavior model of the Event-B model, the growth of state and transitions in the LTS model reflect the actual effect of the addition of guards and actions to the Event-B model. By comparing the graphs, we can see that although the Event-B model has a small amount of code (only 348 lines of Event-B code in the 7th refinement layer), the 74 guards and 49 actions in these codes will produce 2816 states and 16384 transitions into the corresponding LTS model. If we use Rodin to simulate and analyze the transition of the system state, that would be a nightmare. The CSP||B method, the “atomic decomposition” method and the Flow method, can only generate Event-B code and use the similar method (in Rodin environment) to complete the simulation. These methods do not by themselves support the simulation of control flow. Compared to these approaches, we model the system as a series of separated components using the concept of “atomic LTS” which enable people to observe the individual behavior of each component and the interaction between components during system execution, just like in Uppaal [25].

6.3 Comparison of Support for LTL Property Verification

The results of the “atomic decomposition” method and the Flow method cannot be directly converted to LTS models; therefore it is difficult for them to support the verification of LTL properties. The CSPB method is not perfect because the changes of many state variables have not been modeled with CSP. Compared to the CSPB method, we model the behavior of the entire Event-B model as an LTS model. Therefore, our behavior modeling method is more comprehensive than the CSPmethod, which makes the result of our method for LTL properties verification more credible than that of CSPB.

The drawback of LTS model is that it does not support the refinement checking. But we can use Event- B to prevent this flaw. The complementary capabilities of Event-B and LTS allow us to analyze and verify the system’s refinement consistency and behavioral properties from multiple views. This is the idea of the integrated formal method that we are currently advocating.

7. Conclusion

As a reusable formal model, the Event-B design pattern has a very important role for the rapid formal modeling of the system. But it is difficult to model, analyze, verify and preserve the LTL behavior properties of the Event-B model because it lacks behavioral semantics. In this paper, we establish the LTS model of Event-B synchronous control flow design pattern and map the design pattern instantiation process of Event-B to the instantiation process of LTS model. We get the LTS model of a complex multilevel control system using this method and verify its LTL behavior attributes. The experimental data show that it is more convenient to model, analyze and verify the LTL behavior properties of Event-B model if we use LTS as behavior semantic model of Event-B. The LTS behavior semantic model can be a useful complement to the Event-B model.

In the future, we will study how to establish the refinement checking mechanism of the LTS model to ensure the behavior refinement of the Event-B model, which is lacking in the current refinement checking mechanism of Event-B.