# Modelling the Embedded Control System Using iUML-B Pattern State Machine

Authors: Han Peng; Chenglie Du; Lei Rao; Zhouzhou Liu
Journal: Journal of Control Science and Engineering
 (2018)

---

## Abstract

Developing the formal model based on the Event-B design pattern is an excellent method to improve the development efficiency of the embedded control system and improve the reusability of the formal model. However, the instantiation of the Event-B design pattern requires the manual writing of a large number of model codes, which brings a great deal of learning cost and coding burden to the engineering staff. In this paper, we propose a modelling approach for formal development of control systems based on the application of iUML-B state machine patterns to model the four synchronization patterns of the typical control system. Then, we use the instantiation of iUML-B pattern state machine to establish a typical multilevel control system's Event-B model. The simulation results show that the event trace of the model obtained using our method is the same as that of the corresponding model obtained using the traditional Event-B design pattern. Compared with the traditional Event-B design pattern method, our method can greatly reduce the manual coding burden in the modelling process. The system model expressed using the iUML-B pattern state machine can be easily mapped to the labelled transition system so as to verify the behavioural properties of the model.


---

## Body

## 1. Introduction

The embedded control system has been widely used in aviation, aerospace, Internet of things, and cyber-physical system. Due to the complexity of the embedded control system, it is difficult to ensure its safety properties through test and simulation. Therefore, in a variety of safety standards, such as DO-178C [1] and IEC 61508 [2], it has been clearly stated that engineer must use formal methods to model and verify the embedded system.Event-B [3] is a formal modelling language based on set theory and first order logic which is supported by a modern tool and built-in provers. There are a lot of successful cases of Event-B application including aircraft landing gear control system [4] and satellite communication system [5].To improve the reusability of the Event-B model, the researchers proposed the concept of Event-B design patterns [6]. Unlike the software design pattern, the Event-B design pattern is a formal design pattern. The goal of Event-B design patterns is to instantiate some small formal models that have been proven to be correct into actual system models and use these small formal models to construct a larger formal model by model composition. This method not only avoids “reinvent the wheel” but also avoids repetitive refinement and proof.However, according to our experience, one has to add a lot of guards and actions manually if he (she) wants to model the synchronization control flow of control-intensive system using Event-B. It is a heavy work for the modeller. Engineers need an intuitive, simple way to understand and model synchronous control flow patterns.The main contribution of this paper is to show how to use iUML-B pattern state machine to model the synchronization patterns of the control-intensive embedded system and apply it to the Event-B model of the embedded control system. We proposed the concept of iUML-B pattern state machine and developed the pattern state machines of four synchronization patterns (strong synchronization, weak synchronization, strong-strong synchronization, and strong-weak synchronization) for the control-intensive embedded system. Then we establish a formal model of a typical embedded control system by instantiating these four pattern state machines. The experimental results show that, using our proposed method, the modeller can establish a model of the control-intensive embedded system easily according to some simple rules.The remainder of this paper is organized as follows: Section2 describes the related works of the Event-B design pattern. Section 3 introduces the basic knowledge of Event-B and its design patterns and iUML-B state machines. Section 4 uses the iUML-B pattern state machine to model the synchronization patterns of the embedded control system. In Section 5, we instantiated iUML-B pattern state machines into the Event-B model of the embedded control system. In Section 6, we present an evaluation of our approach. Section 7 summarizes the work of this paper and looks ahead to future work.


## 2. Related Work

Event-B design pattern has been widely used in many fields. Renato Silva [7, 8] proposed the design pattern and the “Generic Instantiation” approach and uses this technology to develop the Event-B model of a safety critical subway system. In the instantiation process of the design pattern, the “Generic Instantiation” method can use the rename plug-in to instantiate the design pattern, thus avoiding a lot of repetitive developments and proofs.Abrial [3] proposed four synchronization patterns of embedded control system: strong synchronization, weak synchronization, strong-weak synchronization, and strong-strong synchronization pattern. Its main purpose is to model the “actuator-reactor” patterns of the reactive system. Abrial modelled a mechanical press controller model using these four synchronization patterns. We will introduce these patterns in detail in Section 4. Synchronization pattern is a template for control-intensive embedded systems. It makes modelling of multilayer control systems easy. The modeller needs to instantiate the patterns into the specific model and then composes them together to get a complex multilevel control system model.Sanz Yeganefard [9] applied the monitored, controlled, mode, and commanded (MCMC) method to the control system and proposed four patterns, namely, themonitorpattern,control pattern,mode pattern, andcommandpattern, expressed by Event-B. Sanaz Yeganefard developed the Event-B model of the cruise control system [10], the automotive lane departure warning system [11], and the lane centering controller [12] using the four above-mentioned patterns. In the work of Sanaz Yeganefard, the composition of patterns is proposed to compose the simple patterns into a composition pattern. But the composition of patterns requires tool support.MCMC patterns can be considered as an extended “actuator-reactor” pattern because they add status monitoring to the “actuator-reactor” pattern to form a feedback loop. This is very useful for the development of the formal model of self-adaptive systems.In addition to the typical Event-B design patterns described above, Ali Gondal [13] proposed some Event-B refinement patterns and decomposition/composition patterns to model the product line of feature-oriented control systems. Adisak Intana [14] proposed some Event-B refinement and composition patterns to model wireless sensor networks.To the best of our knowledge, there is no literature on using iUML-B state machine to model the Event-B synchronous control flow patterns.


## 3. Preliminaries

### 3.1. Event-B Model

An Event-B model consists of two parts, machine and context. Context describes the static part of the system, including carrier sets, constants, axioms, and theorems. A machine uses variables and events to describe the changes of the system. The process of developing a system model with Event-B usually begins with an abstract model and then continues to refine the model until it approaches the implementation. In the process of machine refinement, new events and variables can be added step by step. The current development tool for Event-B is the mature Rodin platform [15].In Event-B, an event is made up of the guards and actions parts. An event can usually be expressed asWhen the guards of an event are all satisfied, the event can be triggered and the expression in actions parts describes the change of state variables when an event occurs.


### 3.2. iUML-B State Machine and Its Event Link Function

Snook and Butler invented a “UML-like” Event-B graphical front end, called UML-B [16]. UML-B uses the class diagrams and state diagrams familiar to the software engineers and system engineers to model the system requirements. System model expressed by UML-B can generate the corresponding Event-B machine directly on the Rodin platform. Recently, UML-B has evolved into iUML-B (integrated UML-B), which allows UML-B class diagrams and state diagrams to be embedded directly into an Event-B machine. iUML-B has been successfully applied to some large projects in Europe commission, such as [17–19].The graphical symbol of the iUML-B state machine is similar to the state diagram of the UML, and we need not explain it. What we are interested in is a very powerful feature of the iUML-B state machine; that is, the transition edges in iUML-B state machine can be “linked” with the existing events in the Event-B model to control the order of these events. For example, suppose that we have already written four events:INITIALISATION, a_on, a_off,andb_on. If we want to control the order of these events like “after thea_on event has occurred, theb_on event must occur before thea_off event (Req 1),” then we can create an iUML-B state machine and “link” these four events to the transition edges of the state machine, as shown in Figure 1. The italic codes in Figure 1 are the codes automatically generated by the iUML-B state machine to control the event order.Figure 1
iUML-B state machine of Req 1.We use the definition of “event trace” proposed by Butler [20] to describe the order of events in the Event-B model: “event trace represents a record of a possible execution trace of the model,” and we use ‘∗’ to indicate an event that may occur 0 or more times. An event trace is usually represented by a set of events between “” and “.” For example, e1,e2∗ indicates that the e2 event must be executed after the e1 event occurs, and this event sequence will be repeated indefinitely.


### 3.3. Event-B Design Pattern and Its Instantiation

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. As with the design pattern in software engineering, the Event-B design pattern is an abstract model of a class of problems. For example, the classic “trigger-response” pattern can be expressed in a nonformalized language: “once the trigger eventa_on occurs, then the response eventr_on will be enabled.” Its corresponding Event-B design pattern is shown in Figure 2(a) (we named itP1). Suppose that when the system is initialized, the values ofa andr area0 andr0, respectively. Thenr_on event will be enabled after thea_on event occurs because thea_on event causes the value of variablea to change froma0 toa1, which makes all the guards ofr_on becomeTRUE.Figure 2
Instantiation process of Event-B design pattern.
(a)
Event-B pattern (b)
Renaming rules (c)
Instance of the patternWe can express the “trigger-response” relationship in the specific control system by instantiating the pattern P1. For example, in an actual mechanical control system, there is a relationship between a motor controller button and a motor indicator light: “when the motor controller button is pressed, the motor indicator light must be illuminated.” This relationship is an instance of theP1 pattern. To get this instance, we just need to rename the variables, constants, and event names of the patternP1 according to renaming rules in Figure 2(b). The resulting Event-B model is shown in Figure 2(c) (we named itI1).In this way, the modeller does not have to prove the correctness ofI1 again if he has proven the correctness ofP1. 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.


## 3.1. Event-B Model

An Event-B model consists of two parts, machine and context. Context describes the static part of the system, including carrier sets, constants, axioms, and theorems. A machine uses variables and events to describe the changes of the system. The process of developing a system model with Event-B usually begins with an abstract model and then continues to refine the model until it approaches the implementation. In the process of machine refinement, new events and variables can be added step by step. The current development tool for Event-B is the mature Rodin platform [15].In Event-B, an event is made up of the guards and actions parts. An event can usually be expressed asWhen the guards of an event are all satisfied, the event can be triggered and the expression in actions parts describes the change of state variables when an event occurs.


## 3.2. iUML-B State Machine and Its Event Link Function

Snook and Butler invented a “UML-like” Event-B graphical front end, called UML-B [16]. UML-B uses the class diagrams and state diagrams familiar to the software engineers and system engineers to model the system requirements. System model expressed by UML-B can generate the corresponding Event-B machine directly on the Rodin platform. Recently, UML-B has evolved into iUML-B (integrated UML-B), which allows UML-B class diagrams and state diagrams to be embedded directly into an Event-B machine. iUML-B has been successfully applied to some large projects in Europe commission, such as [17–19].The graphical symbol of the iUML-B state machine is similar to the state diagram of the UML, and we need not explain it. What we are interested in is a very powerful feature of the iUML-B state machine; that is, the transition edges in iUML-B state machine can be “linked” with the existing events in the Event-B model to control the order of these events. For example, suppose that we have already written four events:INITIALISATION, a_on, a_off,andb_on. If we want to control the order of these events like “after thea_on event has occurred, theb_on event must occur before thea_off event (Req 1),” then we can create an iUML-B state machine and “link” these four events to the transition edges of the state machine, as shown in Figure 1. The italic codes in Figure 1 are the codes automatically generated by the iUML-B state machine to control the event order.Figure 1
iUML-B state machine of Req 1.We use the definition of “event trace” proposed by Butler [20] to describe the order of events in the Event-B model: “event trace represents a record of a possible execution trace of the model,” and we use ‘∗’ to indicate an event that may occur 0 or more times. An event trace is usually represented by a set of events between “” and “.” For example, e1,e2∗ indicates that the e2 event must be executed after the e1 event occurs, and this event sequence will be repeated indefinitely.


## 3.3. Event-B Design Pattern and Its Instantiation

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. As with the design pattern in software engineering, the Event-B design pattern is an abstract model of a class of problems. For example, the classic “trigger-response” pattern can be expressed in a nonformalized language: “once the trigger eventa_on occurs, then the response eventr_on will be enabled.” Its corresponding Event-B design pattern is shown in Figure 2(a) (we named itP1). Suppose that when the system is initialized, the values ofa andr area0 andr0, respectively. Thenr_on event will be enabled after thea_on event occurs because thea_on event causes the value of variablea to change froma0 toa1, which makes all the guards ofr_on becomeTRUE.Figure 2
Instantiation process of Event-B design pattern.
(a)
Event-B pattern (b)
Renaming rules (c)
Instance of the patternWe can express the “trigger-response” relationship in the specific control system by instantiating the pattern P1. For example, in an actual mechanical control system, there is a relationship between a motor controller button and a motor indicator light: “when the motor controller button is pressed, the motor indicator light must be illuminated.” This relationship is an instance of theP1 pattern. To get this instance, we just need to rename the variables, constants, and event names of the patternP1 according to renaming rules in Figure 2(b). The resulting Event-B model is shown in Figure 2(c) (we named itI1).In this way, the modeller does not have to prove the correctness ofI1 again if he has proven the correctness ofP1. 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.


## 4. Modelling Synchronous Patterns of the Embedded Control System

In this section, we use the iUML-B pattern state machine to model four typical synchronization patterns in the embedded control system, namely, strong synchronization pattern, weak synchronization pattern, strong-weak synchronization pattern, and strong-strong synchronization pattern. First, we explained in detail four synchronization patterns, which were proposed by Abrial in his book [3]. Then we modelled these four synchronization patterns with the iUML-B state machine.We verify the correctness of our pattern state machine in three steps. First, we compare the Event-B code generated by our pattern state machine and that of the corresponding pattern proposed by Abrial (http://deploy-eprints.ecs.soton.ac.uk/113/3/ch3_pattern.zip). Then we use their corresponding labelled transitions system model to prove that they are equivalent in behaviour. Finally, we compared the event trace of our model with that of Abrial’s Event-B model using the Rodin platform. Simulation results show that the event traces of them are identical.


### 4.1. Synchronization Requirements of Control System

In the embedded control system, the “trigger-response” problem is the simplest and most basic model. In this model, the actuator executes an “action” event and sends an instruction to the reactor. The reactor receives the instruction after the “action” event and executes the “reaction” event, as shown in Figure 3.Figure 3
Actuator-reactor pattern.In this paper, we follow the following naming convention.The variablesa and b represent the state changes of the actuators a and b, respectively. The variables r and s represent the state changes of the reactors r and s, respectively. The eventX_on changes the value of the variable X from 0 to 1, where X∈{a,b,r,s}. The eventX_off changes the value of the variable X from 1 to 0, where X∈{a,b,r,s}.In addition, we refer to an “actuator-reactor” combination as a “subsystem.” For instance, actuatora and reactor r compose a subsystem. We use “uninterruptible trace” to indicate an event trace that cannot be inserted in any other events. For example, if we require e1,e2,e3 to be an uninterruptible trace, then event trace e1,e2,e4,e3 is an illegal trace that deviated from our requirement.(1  ) Strong Synchronization Requirement. A strong synchronization requirement means that once the actuator performs an action, the reactor must respond to it; otherwise, the actuator will not execute any further action. Figure 4 shows this strong synchronization relationship; that is, aftera_onoccurs,r_on must be executed; otherwise, the actuator will wait forever. Similarly, aftera_offoccurs,r_off must be executed. Therefore, the event trace of strong synchronization requirement is a_on,r_on,a_off,r_off  ∗.Figure 4
Strong synchronization requirement.(2  ) Weak Synchronization Requirement. The weak synchronization requirement means that after the actuator executed an action, the reactor may either respond to it or not respond. Thus, the behaviours of the actuator and the responder under the weak synchronization constraint will be the same as in the case of Figure 5. In Figure 5(a), the actuator performsa_on anda_offevents multiple times and the reactor is always in the stater= 0. Figure 5(b) shows the case where the reactor is always in ther = 1 state.Figure 5
Weak synchronization requirement.
(a) (b)(3  ) Strong-Strong Synchronization Requirement. Strong-strong synchronization requirement is the synchronization requirement between two subsystems. Assume that subsystem 1 comprises an actuatora and a reactorr and subsystem 2 comprises an actuatorb and a reactors.The strong-strong synchronization requirement indicates that subsystem 1 and subsystem 2 are strongly synchronous; that is, theb_on event must occur after ther_on event of subsystem 1; otherwise subsystem 1 will wait forever. At the same time, after thes_off event has occurred in subsystem 2, subsystem 1 must executea_off events. This is shown in Figure 6 (Abrial did not give the graphical presentation of strong-strong synchronization patterns in his book [3]. We obtain the graphical representation of the strong-strong synchronization shown in Figure 5 based on the Event-B code of strong-strong synchronous pattern given by Abrial and Figure 3.35 on page 147 in Abrial’s book [3]). The event trace of strong-strong synchronization requirement is unique, that is, a_on,r_on,b_on,s_on,b_off,s_off,a_off,r_off∗.Figure 6
Strong-strong synchronization requirement.(4  ) Strong-Weak Synchronization Requirement. Strong-weak synchronization requirement refers to weak synchronization relationship between subsystem 1 and subsystem 2. Specifically, there are two cases. The first case is that after ther_on event occurs in subsystem 1, the subsequent event may be eitherb_on event in subsystem 2 ora_off event in subsystem 1. The former indicates that subsystem 2 responds to the event of subsystem 1 and enters into an uninterruptible event trace b_on,s_on,b_off,s_off; the latter means that subsystem 2 does not respond to the event of subsystem 1, so subsystem 1 enters its uninterruptible event trace a_off,r_off,a_on,r_on. The principle of strong-weak synchronization is shown in Figure 7(a) (based on the same reason as Section 4.1 (3), we obtain a graphical representation of the strong-weak synchronization pattern according to Figure 3.19 on page 129 in Abrial’s book [3]). The second case is that after thes_off event in subsystem 2 occurs, subsystem 1 may either execute eventa_off to respond to it or may not respond, which will cause subsystem 2 to execute theb_on event and return to its uninterruptible trace b_on,s_on,b_off,s_off. This is shown in Figure 7(b).Figure 7
Strong-weak synchronization requirement.
(a) (b)


### 4.2. Modelling the System Synchronization Pattern with the iUML-B State Machine

In this section, we use iUML-B state machine to model these synchronization patterns. The principle of our approach is to model the actuators and reactors in each design pattern (e.g., the actuatorsa and b and the reactors r and s) as an iUML-B state machine, respectively. Event-B code generated by these state machines is embedded in a single Event-B machine. The resulting Event-B machine is the model for various synchronous control flow patterns. The essence of this procedure is the combination of the state machine of the actuator and the state machine of the reactor, as shown in Figure 8.Figure 8
The principle of modelling.(1  ) Modelling the Weak Synchronization Pattern. According to weak synchronization requirement,r_on must occur aftera_on. Therefore, we first draw the state machines for a and r themselves; then we add a reflexive edge on its statea1 and “link” this edge to eventr_on. Then we can add a reflexive edge on its statea0 and “link” this edge to eventr_off, as shown in Figure 9.Figure 9
The iUML-B state machines of the weak synchronization pattern.
(a)
State machine a (b)
State machine rThe Event-B codes automatically generated according to iUML-B state machines in Figure9 areWe named itWeakiUMLB. To prove thatWeakiUMLB satisfies weak synchronization requirement, we give the Event-B code of weak synchronization proposed by Abrial:We named Abrial’s weak synchronization model asWeakEventB. It is easy to see that the only difference betweenWeakiUMLB andWeakEventB is the value of variablesa andr. According to the algorithm given in literature [21], we convert both models to labelled transitions system (LTS) and get two identical LTSs, as shown in Figure 10.Figure 10
LTS model of weak synchronization pattern.If we only concern the behaviour of the model, that is, the event trace, we can conclude thatWeakiUMLB andWeakEventB are equivalent.In order to confirm the above verification results, we simulated the event traces ofWeakiUMLB andWeakEventB with the aid of the Rodin platform and found that they are identical. Due to space limitations, in the following discussion, we will no longer give the equivalence proof of the other three synchronization patterns.(2  ) Modelling the Strong Synchronization Pattern. According to the requirement of strong synchronization pattern, we modify the state machine of the reactor on the basis of the weak synchronization pattern and add two reflexive edgesa_on anda_off on ther = r0 state andr = r1 state, respectively, as shown in Figure 11.Figure 11
The iUML-B state machines of the strong synchronization pattern.
(a)
State machine a (b)
State machine r(3  ) Modelling the Strong-Weak Synchronization Pattern. We model the strong-weak synchronization pattern using iUML-B state machines as shown in the four subgraphs (a), (b), (c), and (d) in Figure 12. It should be noted that the strong-weak synchronization pattern is the synchronization between the two subsystems, so we need to add more reflexive edge to limit the event order between the subsystems.Figure 12
The iUML-B state machines of strong-weak synchronization pattern.
(a)
State machine a (b)
State machine r (c)
State machine b (d)
State machine s(4  ) Modelling the Strong-Strong Synchronization Pattern. The strong-strong synchronization pattern adds more constraints on the basis of strong-weak synchronization pattern. We added a new auxiliary state machinem to impose these constraints, as shown in Figure 13. We use dotted arrows to point to the Event-B code generated by each edge in the state machinem. It can be seen that the Event-B codes that generated by state machinem in Figure 13 constrained that eventb_on must occur betweena_on anda_offevent.Figure 13
The iUML-B state machinem and the Event-B codes it generated.As we have analyzed in Section4.1 (4), in the strong-weak synchronization pattern, after the event sequence a_on,r_on occurs, both ofa_offevent and ab_on event are enabled. However, after adding a constraint variablem on the strong-weak synchronization pattern,a_off can be enabled only whena = a1 andm = m0. Therefore, in the Event-B model generated by the strong-strong synchronous pattern state machines, after the event sequence <a_on, r_on> occurs, the enabled event can only beb_on. Furthermore, as long asb_on occurs, the system will go into an uninterruptible event trace b_on,s_on,b_off,s_off. Thus, the event trace of this Event-B model can only be a_on,r_on,b_on,s_on,b_off,s_off,a_off,r_off. That is, the strong-weak synchronization pattern state machine becomes the strong-strong synchronization pattern state machine after adding a new state machinem, as shown in Figure 13.


## 4.1. Synchronization Requirements of Control System

In the embedded control system, the “trigger-response” problem is the simplest and most basic model. In this model, the actuator executes an “action” event and sends an instruction to the reactor. The reactor receives the instruction after the “action” event and executes the “reaction” event, as shown in Figure 3.Figure 3
Actuator-reactor pattern.In this paper, we follow the following naming convention.The variablesa and b represent the state changes of the actuators a and b, respectively. The variables r and s represent the state changes of the reactors r and s, respectively. The eventX_on changes the value of the variable X from 0 to 1, where X∈{a,b,r,s}. The eventX_off changes the value of the variable X from 1 to 0, where X∈{a,b,r,s}.In addition, we refer to an “actuator-reactor” combination as a “subsystem.” For instance, actuatora and reactor r compose a subsystem. We use “uninterruptible trace” to indicate an event trace that cannot be inserted in any other events. For example, if we require e1,e2,e3 to be an uninterruptible trace, then event trace e1,e2,e4,e3 is an illegal trace that deviated from our requirement.(1  ) Strong Synchronization Requirement. A strong synchronization requirement means that once the actuator performs an action, the reactor must respond to it; otherwise, the actuator will not execute any further action. Figure 4 shows this strong synchronization relationship; that is, aftera_onoccurs,r_on must be executed; otherwise, the actuator will wait forever. Similarly, aftera_offoccurs,r_off must be executed. Therefore, the event trace of strong synchronization requirement is a_on,r_on,a_off,r_off  ∗.Figure 4
Strong synchronization requirement.(2  ) Weak Synchronization Requirement. The weak synchronization requirement means that after the actuator executed an action, the reactor may either respond to it or not respond. Thus, the behaviours of the actuator and the responder under the weak synchronization constraint will be the same as in the case of Figure 5. In Figure 5(a), the actuator performsa_on anda_offevents multiple times and the reactor is always in the stater= 0. Figure 5(b) shows the case where the reactor is always in ther = 1 state.Figure 5
Weak synchronization requirement.
(a) (b)(3  ) Strong-Strong Synchronization Requirement. Strong-strong synchronization requirement is the synchronization requirement between two subsystems. Assume that subsystem 1 comprises an actuatora and a reactorr and subsystem 2 comprises an actuatorb and a reactors.The strong-strong synchronization requirement indicates that subsystem 1 and subsystem 2 are strongly synchronous; that is, theb_on event must occur after ther_on event of subsystem 1; otherwise subsystem 1 will wait forever. At the same time, after thes_off event has occurred in subsystem 2, subsystem 1 must executea_off events. This is shown in Figure 6 (Abrial did not give the graphical presentation of strong-strong synchronization patterns in his book [3]. We obtain the graphical representation of the strong-strong synchronization shown in Figure 5 based on the Event-B code of strong-strong synchronous pattern given by Abrial and Figure 3.35 on page 147 in Abrial’s book [3]). The event trace of strong-strong synchronization requirement is unique, that is, a_on,r_on,b_on,s_on,b_off,s_off,a_off,r_off∗.Figure 6
Strong-strong synchronization requirement.(4  ) Strong-Weak Synchronization Requirement. Strong-weak synchronization requirement refers to weak synchronization relationship between subsystem 1 and subsystem 2. Specifically, there are two cases. The first case is that after ther_on event occurs in subsystem 1, the subsequent event may be eitherb_on event in subsystem 2 ora_off event in subsystem 1. The former indicates that subsystem 2 responds to the event of subsystem 1 and enters into an uninterruptible event trace b_on,s_on,b_off,s_off; the latter means that subsystem 2 does not respond to the event of subsystem 1, so subsystem 1 enters its uninterruptible event trace a_off,r_off,a_on,r_on. The principle of strong-weak synchronization is shown in Figure 7(a) (based on the same reason as Section 4.1 (3), we obtain a graphical representation of the strong-weak synchronization pattern according to Figure 3.19 on page 129 in Abrial’s book [3]). The second case is that after thes_off event in subsystem 2 occurs, subsystem 1 may either execute eventa_off to respond to it or may not respond, which will cause subsystem 2 to execute theb_on event and return to its uninterruptible trace b_on,s_on,b_off,s_off. This is shown in Figure 7(b).Figure 7
Strong-weak synchronization requirement.
(a) (b)


## 4.2. Modelling the System Synchronization Pattern with the iUML-B State Machine

In this section, we use iUML-B state machine to model these synchronization patterns. The principle of our approach is to model the actuators and reactors in each design pattern (e.g., the actuatorsa and b and the reactors r and s) as an iUML-B state machine, respectively. Event-B code generated by these state machines is embedded in a single Event-B machine. The resulting Event-B machine is the model for various synchronous control flow patterns. The essence of this procedure is the combination of the state machine of the actuator and the state machine of the reactor, as shown in Figure 8.Figure 8
The principle of modelling.(1  ) Modelling the Weak Synchronization Pattern. According to weak synchronization requirement,r_on must occur aftera_on. Therefore, we first draw the state machines for a and r themselves; then we add a reflexive edge on its statea1 and “link” this edge to eventr_on. Then we can add a reflexive edge on its statea0 and “link” this edge to eventr_off, as shown in Figure 9.Figure 9
The iUML-B state machines of the weak synchronization pattern.
(a)
State machine a (b)
State machine rThe Event-B codes automatically generated according to iUML-B state machines in Figure9 areWe named itWeakiUMLB. To prove thatWeakiUMLB satisfies weak synchronization requirement, we give the Event-B code of weak synchronization proposed by Abrial:We named Abrial’s weak synchronization model asWeakEventB. It is easy to see that the only difference betweenWeakiUMLB andWeakEventB is the value of variablesa andr. According to the algorithm given in literature [21], we convert both models to labelled transitions system (LTS) and get two identical LTSs, as shown in Figure 10.Figure 10
LTS model of weak synchronization pattern.If we only concern the behaviour of the model, that is, the event trace, we can conclude thatWeakiUMLB andWeakEventB are equivalent.In order to confirm the above verification results, we simulated the event traces ofWeakiUMLB andWeakEventB with the aid of the Rodin platform and found that they are identical. Due to space limitations, in the following discussion, we will no longer give the equivalence proof of the other three synchronization patterns.(2  ) Modelling the Strong Synchronization Pattern. According to the requirement of strong synchronization pattern, we modify the state machine of the reactor on the basis of the weak synchronization pattern and add two reflexive edgesa_on anda_off on ther = r0 state andr = r1 state, respectively, as shown in Figure 11.Figure 11
The iUML-B state machines of the strong synchronization pattern.
(a)
State machine a (b)
State machine r(3  ) Modelling the Strong-Weak Synchronization Pattern. We model the strong-weak synchronization pattern using iUML-B state machines as shown in the four subgraphs (a), (b), (c), and (d) in Figure 12. It should be noted that the strong-weak synchronization pattern is the synchronization between the two subsystems, so we need to add more reflexive edge to limit the event order between the subsystems.Figure 12
The iUML-B state machines of strong-weak synchronization pattern.
(a)
State machine a (b)
State machine r (c)
State machine b (d)
State machine s(4  ) Modelling the Strong-Strong Synchronization Pattern. The strong-strong synchronization pattern adds more constraints on the basis of strong-weak synchronization pattern. We added a new auxiliary state machinem to impose these constraints, as shown in Figure 13. We use dotted arrows to point to the Event-B code generated by each edge in the state machinem. It can be seen that the Event-B codes that generated by state machinem in Figure 13 constrained that eventb_on must occur betweena_on anda_offevent.Figure 13
The iUML-B state machinem and the Event-B codes it generated.As we have analyzed in Section4.1 (4), in the strong-weak synchronization pattern, after the event sequence a_on,r_on occurs, both ofa_offevent and ab_on event are enabled. However, after adding a constraint variablem on the strong-weak synchronization pattern,a_off can be enabled only whena = a1 andm = m0. Therefore, in the Event-B model generated by the strong-strong synchronous pattern state machines, after the event sequence <a_on, r_on> occurs, the enabled event can only beb_on. Furthermore, as long asb_on occurs, the system will go into an uninterruptible event trace b_on,s_on,b_off,s_off. Thus, the event trace of this Event-B model can only be a_on,r_on,b_on,s_on,b_off,s_off,a_off,r_off. That is, the strong-weak synchronization pattern state machine becomes the strong-strong synchronization pattern state machine after adding a new state machinem, as shown in Figure 13.


## 5. Modelling the Embedded Control System with Pattern State Machine Instantiation

In this section, we instantiate four synchronous pattern state machines and use these instances to build an Event-B model of an embedded control system. In order to prove the simplicity of our method and to compare it with the Event-B design pattern, we used the case of Abrial's mechanical press controller system in chapter 3 of literature [3]. In the remainder of this paper, we refer to this mechanical press controller system as the “Press” system.


### 5.1. System Overview

The principle of Press system is shown in Figure14(a). The system consists of control parts and controlled parts. The controlled parts areMotor,Clutch, andDoor. The control parts are four control buttons. The control buttonsB1 andB2 control the start and stop ofmotor, respectively, andB3 andB4, respectively, control the engage and disengage of theClutch. When theMotor is working, as long asClutch is engaged, theMotor will drive rod; thus slide is driven up and down. Then the tool below the slide will complete the processing of part. TheDoor is to ensure the safety of the staff; that is, when theMotor is working and theClutch is engaged, theDoormust be closed. Likewise, theDoor can be opened only after theClutch is disengaged.Door object is indirectly controlled byB3 andB4.Figure 14
Mechanical press controller system.
(a) (b)The synchronization relationships of Press system are shown in Figure14(b).The relationships between four buttons and thecontroller are weak synchronization. That is, pressing a control button (e.g.,B1) does not guarantee that the corresponding controlled object will respond to it (e.g., theMotor is started). This is because a button may be pressed several times in an instant. But the controlled object can just respond to one of them. The relationship between thecontroller and theClutch (theMotor, theDoor) is a strong synchronization.In addition, there are strong-weak synchronization or strong-strong synchronization relationships between subsystems, as shown in Figure14(b).The strong-strong synchronization relationship between subsystemsSub5andSub7 means that, first, theClutch can be engaged only when theMotor is working; at the same time, theMotor can be stopped only after theClutch is disengaged; second, theMotorcan be stopped and started more than once before theClutch is engaged; similarly, theClutch can be engaged and disengaged multiple times before theMotor is stopped. The strong-strong synchronization relationship between subsystemsSub6 andSub7 is a safety requirement to ensure the safety of the operator. The strong-weak synchronization between subsystemsSub5 andSub6 is similar to the relationship betweenSub5 andSub7.


### 5.2. System Modelling Process

Based on the analysis of the synchronization requirements in Section4.1, we instantiate the four synchronous pattern state machines of iUML-B into the model of the mechanical press controller system. The instantiation of the Event-B design pattern is a renaming process for the variable names, constant names, and the event names of a pattern. We give only examples of instantiation of subsystem 1 (weak synchronization pattern) and subsystem 5-subsystem 7 (strong-weak synchronization pattern); the other subsystems can be instantiated in the same way as these two examples.(  1) Instantiation of the Weak Synchronization Pattern. According to the renaming relation, we get the two instance state machinesstart_motor_button andstart_motor_impulse ofSub1, as shown in Figures 15(a) and 15(b), respectively.Figure 15
Sub1’s instance state machine.
(a)
State machine start_motor_button (b)
State machine start_motor_impulse(  2) Instantiation of Strong-Weak Synchronization Patterns. Strong-weak synchronization pattern is the relationship between subsystems, which is more complex than the internal synchronization of subsystems because they contain the synchronization relationships inside each subsystem and the synchronization relationships between subsystems. Without the help of design pattern, this development will be a painful process. Here, we can get the iUML-B state machines ofSub5 andSub7 just by instantiating the strong-weak synchronization pattern state machines into the instance state machines. We can get four instance state machines ofSub5 andSub7, namely, motor_actuator, motor_sensor, clutch_actuator, andclutch_sensor, as shown in Figure 16.Figure 16
Instance state machines of Sub5 and Sub7.
(a)
State machine motor_actuator (b)
State machine motor_sensor (c)
State machine clutch_actuator (d)
State machine clutch_sensor(  3) Composition of Instance State Machines. To facilitate comparison with traditional design methods, we followed the same refinement approach that has been described by Abrial [3]. We get the iUML-B state machines ofSub1 toSub7 through the instantiation of the pattern state machines and modelled the various synchronization relations between them. The final model of the system consists of 15 iUML-B state machines, of which 14 state machines are shown in Table 1. The 15th state machine is an auxiliary state machine namedm_s6_s7, which is used to model the strong-strong synchronization relationship betweenSub6 andSub7. It is an instance of the state machinem shown in Figure 13.Table 1
Subsystems of Press system and its corresponding iUML-B state machines.
Subsystem iUML-B state machine Synchronization pattern Actuator Reactor Sub1 (B1-controller) start_motor_button start_motor_impulse Weak synchronization Sub2 (B2-controller) stop_motor_button stop_motor_impulse Weak synchronization Sub3 (B3-controller) start_clutch_button start_clutch_impulse Weak synchronization Sub4 (B4-controller) stop_clutch_button stop_clutch_impulse Weak synchronization Sub5 (controller-Motor) motor_actuator motor_sensor Strong synchronization Sub6 (controller-Door) door_actuator door_sensor Strong synchronization Sub7 (controller-Clutch) clutch_actuator clutch_sensor Strong synchronizationAs we said at the beginning of Section4.2, the state machine for each subsystem is actually a composed state machine for two state machines within the subsystem. For example, if we use “⊗” to express the composition of state machines, then we have(1)StateMachinesub1=start_motor_button⊗start_motor_imulseWe can get the state machine for the Press system by the composition of all 15 state machines, which is the composition of all 7 subsystems andm_s6_s7:(2)StateMachinePress=⨂i=17Subi⊗m_s6_s7The ultimate manifestation ofStateMachinePress is the Press system’s Event-B machine.In fact, “composition of iUML-B state machines” here is not “composition of Event-B machines” but an operation similar to the composition of LTSs. In our previous work [22],we have proven that as long as an iUML-B state machine only describes a single variable's change (we refer to this kind of iUML-B state machine as an “atomic state machine”), we can easily convert it to its corresponding LTS model (we call it “atomic LTS”). We have also mapped the composition of iUML-B state machine to that of LTS. That is, if we have multiple atomic state machinesS1, S2... Sn, and their corresponding atomic LTS:LTS (S1), LTS(S2)…LTS(Sn), then we have(3)LTS⨂i=1nSi~∥i=1nLTSSiwhere “∥” represents the composition of LTS and “~” represents the bisimulation equivalence relation between two LTSs.Therefore, according to expression (3), for the iUML-B state machines of this paper, we have(4)LTSStateMachinesub1~LTSstart_motor_button∥LTSstart_motor_imulseand(5)LTSStateMachinePress~∥i=17LTSSubi∥LTSm_s6_s7In this way, we can get the LTS model of an Event-B model, which is obtained by integrating of many iUML-B state machines. Further, it allows us to use a variety of model checking tools to verify the behaviour properties of the Event-B model.


## 5.1. System Overview

The principle of Press system is shown in Figure14(a). The system consists of control parts and controlled parts. The controlled parts areMotor,Clutch, andDoor. The control parts are four control buttons. The control buttonsB1 andB2 control the start and stop ofmotor, respectively, andB3 andB4, respectively, control the engage and disengage of theClutch. When theMotor is working, as long asClutch is engaged, theMotor will drive rod; thus slide is driven up and down. Then the tool below the slide will complete the processing of part. TheDoor is to ensure the safety of the staff; that is, when theMotor is working and theClutch is engaged, theDoormust be closed. Likewise, theDoor can be opened only after theClutch is disengaged.Door object is indirectly controlled byB3 andB4.Figure 14
Mechanical press controller system.
(a) (b)The synchronization relationships of Press system are shown in Figure14(b).The relationships between four buttons and thecontroller are weak synchronization. That is, pressing a control button (e.g.,B1) does not guarantee that the corresponding controlled object will respond to it (e.g., theMotor is started). This is because a button may be pressed several times in an instant. But the controlled object can just respond to one of them. The relationship between thecontroller and theClutch (theMotor, theDoor) is a strong synchronization.In addition, there are strong-weak synchronization or strong-strong synchronization relationships between subsystems, as shown in Figure14(b).The strong-strong synchronization relationship between subsystemsSub5andSub7 means that, first, theClutch can be engaged only when theMotor is working; at the same time, theMotor can be stopped only after theClutch is disengaged; second, theMotorcan be stopped and started more than once before theClutch is engaged; similarly, theClutch can be engaged and disengaged multiple times before theMotor is stopped. The strong-strong synchronization relationship between subsystemsSub6 andSub7 is a safety requirement to ensure the safety of the operator. The strong-weak synchronization between subsystemsSub5 andSub6 is similar to the relationship betweenSub5 andSub7.


## 5.2. System Modelling Process

Based on the analysis of the synchronization requirements in Section4.1, we instantiate the four synchronous pattern state machines of iUML-B into the model of the mechanical press controller system. The instantiation of the Event-B design pattern is a renaming process for the variable names, constant names, and the event names of a pattern. We give only examples of instantiation of subsystem 1 (weak synchronization pattern) and subsystem 5-subsystem 7 (strong-weak synchronization pattern); the other subsystems can be instantiated in the same way as these two examples.(  1) Instantiation of the Weak Synchronization Pattern. According to the renaming relation, we get the two instance state machinesstart_motor_button andstart_motor_impulse ofSub1, as shown in Figures 15(a) and 15(b), respectively.Figure 15
Sub1’s instance state machine.
(a)
State machine start_motor_button (b)
State machine start_motor_impulse(  2) Instantiation of Strong-Weak Synchronization Patterns. Strong-weak synchronization pattern is the relationship between subsystems, which is more complex than the internal synchronization of subsystems because they contain the synchronization relationships inside each subsystem and the synchronization relationships between subsystems. Without the help of design pattern, this development will be a painful process. Here, we can get the iUML-B state machines ofSub5 andSub7 just by instantiating the strong-weak synchronization pattern state machines into the instance state machines. We can get four instance state machines ofSub5 andSub7, namely, motor_actuator, motor_sensor, clutch_actuator, andclutch_sensor, as shown in Figure 16.Figure 16
Instance state machines of Sub5 and Sub7.
(a)
State machine motor_actuator (b)
State machine motor_sensor (c)
State machine clutch_actuator (d)
State machine clutch_sensor(  3) Composition of Instance State Machines. To facilitate comparison with traditional design methods, we followed the same refinement approach that has been described by Abrial [3]. We get the iUML-B state machines ofSub1 toSub7 through the instantiation of the pattern state machines and modelled the various synchronization relations between them. The final model of the system consists of 15 iUML-B state machines, of which 14 state machines are shown in Table 1. The 15th state machine is an auxiliary state machine namedm_s6_s7, which is used to model the strong-strong synchronization relationship betweenSub6 andSub7. It is an instance of the state machinem shown in Figure 13.Table 1
Subsystems of Press system and its corresponding iUML-B state machines.
Subsystem iUML-B state machine Synchronization pattern Actuator Reactor Sub1 (B1-controller) start_motor_button start_motor_impulse Weak synchronization Sub2 (B2-controller) stop_motor_button stop_motor_impulse Weak synchronization Sub3 (B3-controller) start_clutch_button start_clutch_impulse Weak synchronization Sub4 (B4-controller) stop_clutch_button stop_clutch_impulse Weak synchronization Sub5 (controller-Motor) motor_actuator motor_sensor Strong synchronization Sub6 (controller-Door) door_actuator door_sensor Strong synchronization Sub7 (controller-Clutch) clutch_actuator clutch_sensor Strong synchronizationAs we said at the beginning of Section4.2, the state machine for each subsystem is actually a composed state machine for two state machines within the subsystem. For example, if we use “⊗” to express the composition of state machines, then we have(1)StateMachinesub1=start_motor_button⊗start_motor_imulseWe can get the state machine for the Press system by the composition of all 15 state machines, which is the composition of all 7 subsystems andm_s6_s7:(2)StateMachinePress=⨂i=17Subi⊗m_s6_s7The ultimate manifestation ofStateMachinePress is the Press system’s Event-B machine.In fact, “composition of iUML-B state machines” here is not “composition of Event-B machines” but an operation similar to the composition of LTSs. In our previous work [22],we have proven that as long as an iUML-B state machine only describes a single variable's change (we refer to this kind of iUML-B state machine as an “atomic state machine”), we can easily convert it to its corresponding LTS model (we call it “atomic LTS”). We have also mapped the composition of iUML-B state machine to that of LTS. That is, if we have multiple atomic state machinesS1, S2... Sn, and their corresponding atomic LTS:LTS (S1), LTS(S2)…LTS(Sn), then we have(3)LTS⨂i=1nSi~∥i=1nLTSSiwhere “∥” represents the composition of LTS and “~” represents the bisimulation equivalence relation between two LTSs.Therefore, according to expression (3), for the iUML-B state machines of this paper, we have(4)LTSStateMachinesub1~LTSstart_motor_button∥LTSstart_motor_imulseand(5)LTSStateMachinePress~∥i=17LTSSubi∥LTSm_s6_s7In this way, we can get the LTS model of an Event-B model, which is obtained by integrating of many iUML-B state machines. Further, it allows us to use a variety of model checking tools to verify the behaviour properties of the Event-B model.


## 6. Evaluation

In this section, we compared the development method based on iUML-B pattern state machine with the development method based on traditional Event-B design pattern. In general, using iUML-B state machines to model the synchronization control flow patterns has three benefits: (1) iUML-B is as easy as UML to learn and can reduce the manual coding costs; (2) iUML-B state machine can express the control flow explicitly; (3) iUML-B state machine can be easily converted to labelled transition system (LTS).We used the iUML-B pattern state machine to establish the seven-level refinement model of the mechanical press controller system step by step, according to the refinement step that has been described by Abrial [3]. The simulation results on the Rodin platform show that, at each layer, the event trace of the model obtained using our method is the same as that of the corresponding model obtained using Abrial’s traditional design pattern. The growth trend of these elements is shown in Figure 17.Figure 17
Statistics of Press model generated by iUML-B state machine.We use Abrial’s nongraphical model of the Press system (http://deploy-eprints.ecs.soton.ac.uk/113/2/ch3_press.zip), which is a direct hand-coded Event-B model, for comparison with our work. For comparison, we also present the statistical data for the mechanical press controller model developed by the traditional Event-B design pattern. The growth trend of its elements is shown in Figure 18 (the growth trend of variables and invariants in the figure is the same, so the two curves coincide).Figure 18
Statistics of Abrial’s Press model.From the statistical data, we can observe a phenomenon: no matter what method is used to model a control-intensive system, the number of model codes grows fast with the growth of refinement level. For the traditional Event-B design pattern method, the total number of variables, invariants, guards, and actions is 142 when refinement level is 7. For a method based on the iUML-B pattern state machine, this number is 145. From the graphs in Figures17 and 18, it can be seen that the growth rate of guards is the fastest, followed by actions. For more complex multilevel control system, the slope of these two curves will be greater.Although the statistics in Figures17 and 18 are similar, the guards and actions in Figure 17 are automatically generated from the iUML-B state machine and the guards and actions in Figure 18 must be manually coded by the modeller. In other words, using the iUML-B pattern state machine to model control-intensive systems, the amount of manual coding we can save at least is equal to (74 + 49)/142 = 86.6%.Another benefit of our approach is that the control flow of the Event-B model becomes visible. Using the iUML-B state machine, we can express and analyze the event order of the system model easily. And the larger Event-B model is decomposed into smaller subsystems, each with its separated control flow. In this way, the complex multilevel control problem becomes a simple subsystem modelling problem. The final Event-B model is a composition of these subsystems. From the engineering point of view, at the time of decomposing the system, we also decompose the complexity of modelling problems and distribute this complexity to some smaller state machines.Finally, the iUML-B state machine can be easily converted to LTS, so that the behaviour properties of the Event-B model can be analyzed and verified. From the point of view of behavioural semantic verification, this is a very desirable advantage.


## 7. Conclusion and Future Work

In this paper, we use the iUML-B pattern state machine to model the four synchronization design patterns in the embedded control system. Then we instantiate the four iUML-B pattern state machines to get the Event-B model of a complex, multilayer control system. The simulation results show that the event trace of the system model obtained using the iUML-B pattern state machine is the same as that of the model obtained using the traditional Event-B design pattern.The advantage of our approach lies in the following points. First, the process of modelling synchronous control flow patterns is visible. The system’s control flow synchronization patterns are expressed using the iUML-B state machines. This makes the system model be understood more easily. Second, the modelling process of the system becomes simpler. Using the traditional approach based on the Event-B design pattern, the modeller who wants to add a new control flow needs to find the locations in hundreds or even thousands of lines of code to insert the guards and actions. However, using the iUML-B pattern state machine, people only need to add some transition edges in a state machine to complete these tasks. Finally, the decomposition and composition of the subsystems are visible. The system’s control flow model is decomposed into some iUML-B state machines, and each pair of iUML-B state machines forms a subsystem. The final system model is the composition of these iUML-B state machines.Event-B is a data-oriented formal modelling language. Therefore, it cannot guarantee the consistency of behaviour between the refined model and the abstract model. In the future, we want to propose an integrated formal method that can guarantee the consistency of the refined model and abstract model in both behaviour aspect and data aspect.



---

*Source: 1468172-2018-06-12.xml*