CS计算机代考程序代写 concurrency Java case study distributed system IEICE TRANS. ??, VOL.Exx–??, NO.xx XXXX 200x

IEICE TRANS. ??, VOL.Exx–??, NO.xx XXXX 200x
PAPER
Real-time System Modeling and Verification through Labeled Transition System Analyser (LTSA)
Yilong YANG†a), Member, Xiaoshan LI†b), and Quan ZU†c), Nonmembers
DOI: 10.1587/trans.E0.??.1
Copyright © 200x The Institute of Electronics, Information and Communication Engineers
1
SUMMARY With the advancement of software engineering in recent years, the model checking techniques are widely applied in various areas to do the verification for the system model. However, it is difficult to apply the model checking to verify requirements due to lacking the details of the design. Unlike other model checking tools, LTSA provides the structure diagram, which can bridge the gap between the requirements and the design. In this paper, we demonstrate the abilities of LTSA shipped with the classic case study of the steam boiler system. The structure diagram of LTSA can specify the interactions between the controller and the steam boiler, which can be derived from UML requirements model such as system sequence diagram of the steam boiler system. The start-up design model of LTSA can be generated from the structure diagram. Furthermore, we provide a variation law of the steam rate to avoid the issue of state space explosion and show how explicitly and implicitly model the time that reflects the difference between system modeling and the physical world. Finally, the derived model is verified against the required properties. Our work demonstrates the potential power of integrating UML with model checking tools in requirement elicitation, system design, and verification. keywords: LTSA,modelchecking,steamboiler,UML
1. Introduction
Real-time computing [1] describes hardware and software systems depending not only on the logical correctness of computation but also on the time constraints. The critical real-time systems must be dependable because any failure of the system could cause an economic disaster or even loss of human lives. The safety properties of such systems must be verified in the design stage as well as the testing stage of development before any deployment. Formal methods [2][3] provide promising approaches to verify the safety properties of system. The papers [4][5][6] provide the case studies of general railroad crossing problem, pacemaker, and cell phone, to illustrate how to verify the safety properties of the real-time systems. Unlike mathematical approach to prove safety properties, model checking [7] is a promising ap- proach, which can automatically verify the safety properties by exploring the state space of the target system. For exam- ple, UPPAAL [8] is one of the successful model checking tools widely applied to various areas from communication protocols to multimedia applications, in particular to the real-time system. When using UPPAAL for verifying the target system, the components of the system are abstractly
†The author is with the department of computer and information science, faculty of science and technology, university of Macau, Macau
a) E-mail: yylonly@gmail.com b) E-mail: xsl@umac.mo
c) E-mail: quanzu@umac.mo
modeled as finite state machines based on the theory of timed automata [9]. The advantages are more intuitive and easier understanding while modeling the real-time system as state machines. However, representing state machines graphically severely limits the complexity of problems that can be addressed. Consequently, textual process calculuses such as Calculus of Communicating Systems (CCS) [10] and Communicating Sequential Processes (CSP) [11] as the compensations of the finite state machine are usually used for modeling complex systems.
In this paper, we use Labeled Transition System Anal- yser (LTSA) to model real-time systems and verify safety properties [12]. Because LTSA contains many charming fea- tures: 1) LTSA provides both graphic state machine and tex- tual process calculus, Finite State Processes (FSP), to model systems. 2) A textual process model can be automatically transformed to the corresponding graphic state machine. 3) LTSA can describe system architectures by structure dia- grams (simplified form of the graphical representation of Darwin [13]), which can describe the high-level model de- sign and the static structure. 4) The skeleton of process model can be automatically generated from system archi- tectures for the next round fine-grained design [14]. One interesting work [15] proposes a method to detect refine- ment errors in UML sequence diagrams using LTSA. That demonstrate the power the LTSA for UML model checking.
Although LTSA has many advantages for modeling sys- tem, there are few examples of real-time systems modeling through LTSA. The steam boiler [16][17] is a classic case study for real-time system modeling in many studies. The steam boiler is the minimal real-time system that contains all the essential parts of a real-time system: a controller and a controlled object with the sensors and the actuators. The controller can periodically sample the state of the con- trolled object by the sensors, then strategically change the state of the controlled object through the actuators to guar- antee the safety of the whole system. All the components of the real-time system are synchronized through time. In the physical world, time is implicitly contained in the phys- ical phenomenon; e.g., the current temperature of the water was determined by the heating power and the heating time. Therefore, when modeling the real-time system, the time should be considered as inside of physical law of the con- troller object. However, for abstraction of the physical world and easy understanding, many studies explicitly model the time as a component of the system named timer, and then use that timer component to synchronize with other components
arXiv:1803.05362v1 [cs.SE] 14 Mar 2018

2
of the system.
Related Work: As a classic real-time system, the steam boiler has been widely studied. The paper [18] presents a for- malization of the steam boiler problem using Circus, which is a unified theory of Z and CSP. It utilizes the strength of Z notation to describe the specifications of the system and their refinement, the strength of CSP to describe and reason about concurrency. Using Timed Automata to solve the steam boiler problem is mentioned in [19], which describes time constraints in the model with clocks. The guards may enable or disable transitions according to clock values. Mean Value Calculus models the steam boiler in [20], which could be used to specify and reason about time and logical constraint of the real-time system. Other related case studies for model- ing and verifying real-time system are: Spin [21] Signal-coq [22], Action System [23], PLUSS [24],FOCUS [25], LO- TOS [26] and Hybrid Relation Calculus [27]. Although the steam boiler problem has been elaborately studied, almost all case studies above have the following defects: 1) they explicitly model time as a timer component, that will make a gap between the real-time system design and the physical real-time system. 2) they do not provide a variation law for the steam rate, that will lead to the issue of state space ex- plosion. 3) they do not contain any diagram to describe the system architecture, that will make it hard to directly elicit the components from target problem.
Contributions: Although some tools support implicit time modeling inside of the system, to our best knowledge, there is no related work to illustrate the differences between the im- plicit timer and explicit timer, and the relationship between the physical world timer and timer in the real-time modeling. the Contributions of our paper are:
1) Demonstrating LTSA modeling and verifying abilities for real-time system shipped by a classical steam boiler problem.
2) Demonstrating how to specify structure diagram from UML requirement model, then generate the sketch of design model from structure diagram by Darwin.
3) Providing a variation law for the steam rate to avoid the issue of state space explosion.
4) Discussing how to model the explicit and implicit timer in the real-time system, and the relationship of time between the system modeling and physical world.
The remainder of this paper is organized as follows: Section 2 is preliminary of FSP specification and overviews the steam boiler problem. Section 3 shows the interaction requirements and the derived structure diagram. Section 4 presents how to model the steam boiler in LTSA, especially for the time modeling. And then Section 5 shows the LTSA verification and simulation. Finally, section 6 concludes this paper and puts forward the future work.
2. Preliminary
LTSA adopts FSP as textual model to describe the system. To
make this paper self-contained, we present the specification of FSP and the brief introduction of steam boiler problem in this section. More details of FSP could be found in the textbook [12].
2.1 The Specification of FSP
Finite State Process (FSP) is CSP syntax-liked formal lan- guage for modeling concurrency system [12], it uses concept of Primitive Process to define the component of the system which may contain the sequences of actions. Component composition could be defined as Composited Processes in which concurrent executions of actions could be synchronied or interleaved. The requirements of system could be captured as the Properties of FSP. Once both properties and processes of the system are defined, LTSA can check the satisfiability of properties for particular system. The brief summary of FSP specification is provided as follows:
Primitive Process A primitive process is the execution of a sequential program. The state of primitive process is trans- formed by executing actions. We use primitive process to define the component of the system. Like any programming languages, primitive process may contain choice expression, condition,
• Action Prefix ->: (a -> P) describes a process which engages in the action a and then behaves as described byP.
• Choice |: (a -> P | b -> Q) describes a process which initially engages in either of the actions a or b. After the first action has been performed, the subsequent be- haviour is described by P if the first event was a, or by Q if the first event was b.
• STOP: It is sometimes (if rarely) necessary to specify a primitive process which terminates. Consequently, a local process STOP is predefined which engages in no further actions.
• Alphabet Extension +{}: Each primitive process has an alphabet consisting of the actions it may take part in. A process may only engage in the actions contained in its alphabet although the converse does not hold. It is sometimes useful to extend the alphabet of a process with actions that it does not engage in and consequently actions that are not used in its definition. This may be done to prevent another process executing the action.
• Indexing: Both local process names and action names may be indexed. Both local processes and actions may have more than one index as illustrated by this example (for actions). A process which outputs the sum of two integers (in the range 0..N).
• Conditional: A conditional takes the form: if expr then local_process else local_process.
• Guards: A guarded transition takes the form (when B a -> P) which means that the action a is eligible when the guard B is true, otherwise a cannot be chosen for execution.
IEICE TRANS. ??, VOL.Exx–??, NO.xx XXXX 200x

YANG et al.: REAL-TIME SYSTEM MODELING AND VERIFICATION THROUGH LABELED TRANSITION SYSTEM ANALYSER (LTSA)
Composited Processes Parallel Composition ∥: (P ∥ Q) expresses the parallel composition of the processes P and Q. It allows all the possible interleavings of the actions of the two processes. These shared actions synchronise the execution of the two processes. If the processes contain no shared actions then the composite state machine will describe all interleaving.
Safety Properties A safety property asserts that nothing bad happens. Informally, a property process specifies a set of acceptable behaviours for the system it is composed with. A system S will satisfy a property P if S can only generate sequences of actions (traces) which when restricted to the alphabet of P, are acceptable to P.
Progress Properties A progress property asserts that it is always the case that an action is eventually executed. We will define progress to check the steam boiler is still work or not.
2.2 Steam Boiler Problem
The steam boiler problem [16][17] is one of the typical prob- lems in software engineering, which divides the system into physical and control parts. For the physical part, it has a physical steam boiler, three water/steam/pump sensors and pumps. For the control part, it is a controller which could get the value from the sensors, make a decision, and send orders of switching on/off to the pumps. The communication between physical and control parts are messages.
Table 1: The Summary of Constants and Variables
the steam boiler. M1 is minimal limit of water quantity, M2 is maximal limitation, N1 is minimal limitation and N2 is maximal limitation in normal mode, W is maximal quantity of outcome steam, the increase rate of outcome steam are defined by U1, the decrease rate of outcome steam is U2, the number of pumps is 5, P is capacity of each pump.
System constants must satisfy the in-equation: 0 TIMER)
where each tick represents the pass of one second.
If the sampling period is identical with the delay of pumping, which is the case in the steam boiler specifica- tion[16], we can model the system in a time-implicit way. That is, we don’t need a Timer component to explicitly spec- ify the time passing. We compare these two different mod-
eling methods in the next subsection.
4.2 Steam Boiler Component
The specification[16] specifies part of the behaviours in the steam boiler system. For instance, after switching on the pump, the water starts pouring into the boiler in 5 seconds. But some details are not given, including the variation law of the steam rate and the control strategy of the pump. We design a pumping control strategy in next subsection. In this subsection, we hypothesize a physical variation law for the steam rate and show the model of the steam boiler in FSP.
4.2.1 Quantity of Water
We use qi, vi, pi to respectively denote the steam rate, the quality of water, and the pumping rate at the ti time point. Then clearly we have the following equation:
(3) qi+1 =qi +(pi −vi)∗∆t where ∆t = 1.
4.2.2 Steam Rate
The hypothesis of the law of the steam rate is based on the fact that the steam rate is influenced by the quantity of the water. Between N1 and N2, we add another two quantities of water level B1 and B2, the best minimal limit and the best maximal limit, which are used to construct
IEICE TRANS. ??, VOL.Exx–??, NO.xx XXXX 200x
tick
tick
tick
STEAM SENSOR getSteamRate
PUMP getPumpRate SENSOR
WATER SENSOR
getWaterQuantity
waterchan
steamchan pumpsensorchan
getSteamRate
getPumpRate
getWaterQuantity
tick
STEAM BOILER
pumpOn pumpOff keep
repaired
pumpOn
pumpOff PUMP keep
pumpcontrollerchan
rescue
CONTROLER

YANG et al.: REAL-TIME SYSTEM MODELING AND VERIFICATION THROUGH LABELED TRANSITION SYSTEM ANALYSER (LTSA)
the hypothesis. We use VMINOUT to denote the minimal steam rate. It is required that (N1 < B1 < B2 < N2) and 0 0), or if current water level ii
is between B2 and N2 and it is decreasing (pi − vi < 0), the steam rate will have an increment of U1. If current water level is between N1 and B1 and it is decreasing (pi − vi < 0), or if current water level is between B2 and N2 and it is increasing (pi − vi > 0), the steam rate will have a decrement of U2.
and 00101 means the pump will increase now and in 3 sec- onds. We assume that there is at most one pump opening in one second. Once receiving the action pumpOn, the first bit of the sequence will be set to 1. In each second, the sequence will move one position to the right, representing one second elapses.
4.2.4 Steam Boiler in FSP
STEAMBOILER has two subcomponents STEAMBOILERUN and PUMPDELAY. The sensors get the measures from the steam boiler by the actions getPumpRate, getSteamRate and getWaterQuantity. The steam boiler communicates with the pump by the actions pumpOn, pumpOff and keep. If pumpOff, the pump rate decreases immediately. If pumpOn, t is increased by 16, which is 10000 in binary. The steam boiler synchronizes with Timer by the action tick. In each second, the quantity of the water is changing according to Formula 3 and the steam rate changes according to the law. The pumping rate will be checked in PUMPDELAY. It firstly checks whether the last bit is 1, representing current incre- ment. Then it moves the sequence one position to the right by the division by 2. The following is part of the model.
1 STEAMBOILER = (start->STEAMBOILERUN[INITQ][W][PUMPQ][0]), 2 STEAMBOILERUN[q:Q][v:V][p:PUMPQ][t:PUMPMAXDELAY] = (
(4) vi+1 =


vi − U2
vi−U2
if B2 ≤ qi < N2 and pi − vi > 0
ifN10 1i1ii
ifB ≤q ≤B 1i2

VMINOUT ifN ≤q ≤Cor0≤q ≤N 2ii1
4.2.5 Throughput of pumps in implicit time
In the case of the sampling period is identical with the pump- ing delay time, we can use the implicit way to model the system. For the function of p, when the action pumpOn is triggered at ti, the fixed delay is required before p is changed. Therefore, p is unchanged from the time point ti to ti+4. The value of pi+5 is determined by the fol- lowing factors: 1) pi, 2) whether the last pump order lastpo ∈ {True, False} is pumpOn or not, 3) the previous or- der actionp ∈ {pumpOn, pumpOff, keep}, and 4) the current order actionc ∈ {pumpOn, pumpOff, keep} of the pump.
vi+U1 


v +U i1
W 
4.2.3 Throughput of pumps
It is specified that, after switching on, the pump needs 5
seconds to pour the water into the boiler. That is, assuming
the action pumpOn is trigger at t , the pumping rate p will i
have a increment of P at t . To model this time delay, i+5
we use a sequence of 5 bits to represent the time points at which the pump rate will increase. Each bit in the sequence represents the action in the corresponding time point. For instance, 10000 means the pump will increase in 5 seconds,
pi 

 p i
 p i

 i p

 p i
+ P + P
if lastpo = True and actionc = pumpOn if lastpo = True and actionc = keep
if lastpo = True and actionc = pumpOff if lastpo = False and actionc = pumpOn if lastpo = False and actionc = keep
if lastpo = False and actionc = pumpOff Otherwise
3
4
5 | 6 | 7 | 8 | 9
getWaterQuantity[q] -> getSteamRate[v]
-> getPumpRate[p] -> STEAMBOILERUN[q][v][p][t]
pumpOn -> STEAMBOILERUN[q][v][p][16+t] pumpOff -> STEAMBOILERUN[q][v][p-PQ][t] keep -> STEAMBOILERUN[q][v][p][t]
tick -> (
| when (BEST2 < q && q < N2 && (p-v) < 0 && (v+UP) < W) boilingBEST2toN21[q][v][p] -> PUMPDELAY[q+(p-v)][v+UP][p][t] …… ) ),
(5)
(6)
pi+5 =
when (q >= N2 )
boiling -> PUMPDELAY[q+(p-v)][VMINOUT][p][t]
10
11
12
13
14 PUMPDELAY[q:Q][v:V][p:P][t:PUMPMAXDELAY] = (
15 when (t % 2 == 0) pumping -> STEAMBOILERUN[q][v][p][t/2]
16 | when (t % 2 != 0) pumping -> STEAMBOILERUN[q][v][p][(t-1)/2]).
􏰄pi − P pi+1 = pi
5
C
M2
N2
B2 B1
N1 M1
0
v = VMINOUT
v = V – U2
v = V + U1
v =W
v = VMINOUT
v = V + U1
v = V – U2

6
(7)
lastpo =
􏰄True if actionp = pumpOn
False if actionp ∈ {keep, pumpOff }
If the last order is pumpOn and current order is pumpOn, pi+5 is pi plus P. If the last order is pumpOn and current order is keep, pi+5 is pi plus P. If the last order is pumpOn, and current order is pumpOff, pi+5 will not change. It is same in the case that if the previous order is not pumpOn and current order is pumpOn or keep. pk+1 is pk minus P, if the last order is not pumpOn and current order is keep. The reader may refer to the details of the implicit model in our website† .
4.3 Sensor Components
Sensor devices measure the state of the steam-boiler and the value of the measures are transmitted to the control sys- tem through network or cable. The measure processes are modelled as the synchronizations between STEAM BOILER and the sensor components, and the transmissions are mod- eled as the synchronizations between CONTROLLER and the sensor components. Sensor components FSP processes are described as below:
WATERSENSOR = ( getWaterQuantity[q:Q] -> waterchan.send[q] -> tick -> tick -> tick -> tick -> tick -> WATERSENSOR).
STEAMSENSOR = ( getSteamRate[v:V] -> steamchan.send[v] -> tick -> tick -> tick -> tick -> tick -> STEAMSENSOR).
PUMPSENSOR = ( getPumpRate[p:5*P] -> pumpsensorchan.send[p] -> tick -> tick -> tick -> tick -> tick -> PUMPSENSOR).
4.4 Pump Component
The pump controller component is defined as:
PUMPCONTROLLER = (pumpcontrollerchan.receive[o:PUMPORDER] -> (when (o == ON) pumpOn -> PUMPTICK |
when (o == OFF) pumpOff -> PUMPTICK |
when (o == KEEP) keep -> PUMPTICK)),
PUMPTICK = (tick -> tick -> tick -> tick -> tick -> PUMPCONTROLLER).
Fig. 4: Pump Component in LTSA
ON if q < B1 + FTRD and p ≤ 3P   ON if q < B1 + FTRD and p = 4P and lastpo = False    KEEP ifq pumpsensorchan.receive[p:5*P] -> 4 makedecision ->
5 ———————- q < BEST1+FTRD ————————- 6 ( when (q < BEST1+FTRD && p <= 3*P)) 7 pumpcontrollerchan.send[ON] -> CONTROLTICK[True][q]
8 | when (q < BEST1+FTRD && p == 4*P && lastpo == False) 9 pumpcontrollerchan.send[ON] -> CONTROLTICK[True][q]
do the action makedecision to generate an order o, then do 22
action pumpcontrollerchan.send[o] to send order o to pump controller channel, function o is defined as:
† http://lab.mydreamy.net
23 24 25
CONTROLTICK[o:PUMPORDER][q:Q] = (tick -> tick -> tick -> tick -> tick -> SYSCONTROLRUN[o][q]).
The boundary situations are in Line 17-18 and Line 25-26, and when the pumpOn decision is made, the control system


 KEEP 


 KEEP
OFF
ifB1+FTRD≤q≤B2−FTRU ifq>B2+FTRUandv≥0andp=0 ifq>B2+FTRUand(p−v)≥0andp>0
IEICE TRANS. ??, VOL.Exx–??, NO.xx XXXX 200x
Because of the delay of pumping, thresholds of FTRD and FTRU are introduced (0 ≤ FTRD ≤ B2 − B1, 0 ≤ FTRU ≤ B2 − B1). If the water level is above B2 plus FTRU, and the water level is not decreasing and the pump rate is greater than zero, the decision OFF is made. If the water level is under B1 + FTRD, and either throughout of pumps is less than 3P or throughout of pumps is 4P without the previous order pumpON, the decision is ON. The decision is KEEP, if water level is between that two boundaries, or water level is above B2 plus FTRU besides steam rate is great than zero, throughput of pumps is zero, or water level is under B1 plus FTRD besides throughput of pumps is maximal or 4P and previous order is pumpOn. Controller component of FSP is:
CONTROLSYSTEM = (init -> SYSCONTROLRUN[OFF]), SYSCONTROLRUN[po:PUMPORDER] = (waterchan.receive[q:Q] ->
10 | when (q < BEST1+FTRD && p <= 4*P && lastpo == True) 11 pumpcontrollerchan.send[KEEP] -> CONTROLTICK[False][q]
12 | when (q < BEST1+FTRD && p == 5*P) 13 pumpcontrollerchan.send[KEEP] -> CONTROLTICK[False][q]
14 ——————— q > BEST2-FTRU ————————–
15 | when (q > BEST2-FTRU && (p-v) >= 0 && p > 0)
16 pumpcontrollerchan.send[OFF] -> CONTROLTICK[False][q]
17 | when (q > BEST2-FTRU && v >= 0 && p == 0)
18 pumpcontrollerchan.send[KEEP] -> CONTROLTICK[False][q]
19 —————-BEST1+FTRD <= q && q <= BEST2-FTRU————– 20 | when (BEST1+FTRD <= q && q <= BEST2-FTRU) 21 pumpcontrollerchan.send[KEEP] -> CONTROLTICK[False][q])),

YANG et al.: REAL-TIME SYSTEM MODELING AND VERIFICATION THROUGH LABELED TRANSITION SYSTEM ANALYSER (LTSA)
of FSP takes previous order into account in Line 8-18.
5. Model Verification and Simulation
This section verifies the FSP model against the safety prop- erties and the progress properties in LTSA. Safety property checking guarantees that there is no deadlock in the system and the water quantity level keeps in the specified ranges. Progress property checking guarantees that there is no local loop in the system state.
5.1 Requirement specified by FSP
Safety Property For safety checking, basic and normal prop- erties according to Requirement 1 and 2 are defined for a different mode. FSP does not provide a mechanism for de- scribing invariant directly. Hence, actions with parameter are used to describe invariants. Basic property is described as getWaterQuantity[q:M1..M2], which requires that water quantity q must be maintained between M1 and M2, normal property as getWaterQuantity[q:N1..N2] requires that water quantity q must be retained between N1 and N2:
property BASIC = (getWaterQuantity[q:M1..M2] -> BASIC)
+ {getWaterQuantity[0..M1-1], getWaterQuantity[M2+1..C]}.
property NORMAL = (getWaterQuantity[q:N1..N2] -> NORMAL)
+ {getWaterQuantity[0..N1-1], getWaterQuantity[N2+1..C]}.
property OPTIMIZATION = (getWaterQuantity[q:BEST1..BEST2] -> OPTIMIZATION) + {getWaterQuantity[0..BEST1-1], getWaterQuantity[BEST2+1..C]}.
Notes: Optimization property is defined for checking our model works. In the normal mode, our model must not vio- late basic and normal properties, but optimization property. In the rescue mode, our model must not violate basic prop- erty within constraint the time, but normal and optimization properties.
Progress Property In our case, the steam boiler system is in progress, when actions of boiling and boiling out of the steam boiler, makedecision of the controller, get water quan- tity of water sensor, get the steam rate of the steam sensor, pumpOn and pumpOff of pumps are eventually executed. Those properties are defined:
progress WaterSensorWorking = {getWaterQuantity[q:Q]}
progress SteamSensorWorking = {getSteamRate[v:V]}
progress PumpSensorWorking = {getPumpRate[v:V]}
progress PumpControllerWorking = {pumpOn, pumpOff, keep} progress CSWorking = {makedecision, makerescuedecision, rescue,
repaired}
progress STEAMBOILERWorking = {boiling[q:Q][v:V][p:P],
boilingout[q:Q][v:V][p:P]}
The defined properties must be compositied with SYS- TEMDESIGN for verification:
||BASICSYSTEM = (SYSTEMDESIGN || BASIC). ||NORMALSYSTEM = (SYSTEMDESIGN || NORMAL). ||OPTIMIZATIONSYSTEM = (SYSTEMDESIGN || OPTIMIZATION).
After compositied, the processes BASICSYSTEM, NORMAL- SYSTEM, and OPTIMIZATIONSYSTEM will be verified in LTSA tools.
5.2 LTSA Verification
In this section, FSP model of the steam boiler is loaded into LTSA† (Labelled Transition System Analyser) for verifica- tion. We use the standalone version 3.0, the eclipse plugin could use as the same way as well. NORMAL property N1 ≤ q ≤ N2 is checked as follows:
The result in Fig 5 shows all the components are com- piled, then components are composited with NORMAL prop- erty, and NORMALSYSTEM is not violated the NORMAL
property.
The progress of NORMALSYSTEM is checked:
7
Fig. 5: Verification for Normal Property
Progress Check…
— States: 409 Transitions: 870 Memory used: 1633516K
No progress violations detected.
Progress Check in: 6ms
The deadlock of NORMALSYSTEM is checked here:
Analysing…
— States: 409 Transitions: 870 Memory used: 1544363K
No deadlocks/errors
Analysed using Supertrace in: 23ms
This the result shows no deadlock and progress issue and normal property is hold in this model. The LTSA can also provides the violation traces. The violations case can be found in our website. Furthermore, we make our model open access on Github††, you can download and check the model, and make a contribution by sending a pull request, if needed.
6. Conclusions and Future Work
In this paper, a nontrivial case study is presented to demon- strate how LTSA modeling and verifying the real-time sys- tem. We show how to specify the structure diagram from UML requirement model, and then generate the start-up de- sign model from the structure diagram. Furthermore, we represent a variation law for the steam rate to prevent the problem of state space explosion. We illustrate how to model the explicit and implicit timer in the components of steam boiler system. For the most important effect of our paper, we show the potential power of integrating UML with the model
† http://www.doc.ic.ac.uk/ltsa/ ††https://github.com/yylonly/LTSA

8
checking tools in requirement elicitation, system design and verification.
In the future, we consider to integrate LTSA with our code generation tools RMCode [28] to support verifying the requirement model. Furthermore, we consider generate code directly from the verified FSP model. Hopefully, this paper should be useful for in industry and academic worlds.
Acknowledgment
This work was supported by the National Natural Science Foundation of China (Grant No. 61562011) and the Macau Science and Technology Development Fund (FDCT) (Grant No. 103/2015/A3).
References
[1] K.G. Shin and P. Ramanathan, “Real-time computing: A new dis- cipline of computer science and engineering,” Proceedings of the IEEE, vol.82, no.1, pp.6–24, 1994.
[2] T.ODA,K.ARAKI,andP.G.LARSEN,“Aformalmodelingtoolfor exploratory modeling in software development,” IEICE Transactions on Information and Systems, vol.100, no.6, pp.1210–1217, 2017.
[3] S. Saeeiab and M. Saeki, “Method integration with formal descrip- tion techniques,” IEICE TRANSACTIONS on Information and Sys- tems, vol.83, no.4, pp.616–626, 2000.
[4] C.L.Heitmeyer,B.Labaw,andR.Jeffords,“Abenchmarkforcom- paring different approaches for specifying and verifying real-time systems,” tech. rep., DTIC Document, 1993.
[5] M. Pajic, Z. Jiang, I. Lee, O. Sokolsky, and R. Mangharam, “From verification to implementation: A model translation tool and a pace- maker case study,” Real-Time and Embedded Technology and Ap- plications Symposium (RTAS), 2012 IEEE 18th, pp.173–184, IEEE, 2012.
[6] F.Calabrese,M.Colonna,P.Lovisolo,D.Parata,andC.Ratti,“Real- time urban monitoring using cell phones: A case study in rome,” Intelligent Transportation Systems, IEEE Transactions on, vol.12, no.1, pp.141–151, 2011.
[7] M.M.Ben-Ari,“Aprimeronmodelchecking,”ACMInroads,vol.1, no.1, pp.40–47, March 2010.
[8] G. Behrmann, A. David, and K.G. Larsen, A Tutorial on Uppaal, pp.200–236, Springer Berlin Heidelberg, Berlin, Heidelberg, 2004.
[9] R. Alur and D. Dill, Automata for modeling real-time systems, pp.322–335, Springer Berlin Heidelberg, Berlin, Heidelberg, 1990.
[10] R.Milner,Communicationandconcurrency,PrenticehallNewYork etc., 1989.
[11] C.A.R. Hoare, Communicating Sequential Processes, pp.413–443,
Springer New York, New York, NY, 2002.
[12] J. Magee and J. Kramer, State models and java programs, wiley,
1999.
[13] J. Magee, N. Dulay, and J. Kramer, “Regis: a constructive devel-
opment environment for distributed programs,” Distributed Systems
Engineering, vol.1, no.5, p.304, 1994.
[14] J. Magee, J. Kramer, and D. Giannakopoulou, “Analysing the be-
haviour of distributed software architectures: a case study,” Pro- ceedings of the Sixth IEEE Computer Society Workshop on Future Trends of Distributed Computing Systems, pp.240–245, Oct 1997.
[15] H.Miyazaki,T.Yokogawa,S.Amasaki,K.Asada,andY.Sato,“Syn- thesis and refinement check of sequence diagrams,” IEICE TRANS- ACTIONS on Information and Systems, vol.95, no.9, pp.2193–2201, 2012.
[16] J.R.Abrial,“Steam-boilercontrolspecificationproblem,”inFormal Methods for Industrial Applications, pp.500–509, Springer, 1996.
[17] J.R. Abrial, E. Börger, and H. Langmaack, Formal methods for in- dustrial applications: Specifying and programming the steam boiler control, Springer Science & Business Media, 1996.
[18] J.WoodcockandA.Cavalcanti,“Thesteamboilerinaunifiedtheory of z and csp,” apsec, p.291, IEEE, 2001.
[19] G.LeebandN.Lynch,“Provingsafetypropertiesofthesteamboiler controller,” in Formal Methods for Industrial Applications, pp.318– 338, Springer, 1996.
[20] X. Li and J. Wang, “Specifying optimal design for a steam-boiler system,” in Formal Methods for Industrial Applications, pp.359– 378, Springer, 1996.
[21] S.LöfflerandA.Serhrouchni,“Creatingavalidatedimplementation of the steam boiler control,” 1997.
[22] M. Kerboeuf, D. Nowak, and J.P. Talpin, “Specification and veri- fication of a steam-boiler with signal-coq,” in Theorem Proving in Higher Order Logics, pp.356–371, Springer, 2000.
[23] M. Butler, E. Sekerinski, and K. Sere, “An action system approach to the steam boiler problem,” in Formal Methods for Industrial Ap- plications, pp.129–148, Springer, 1996.
[24] M.C. Gaudel, P. Dauchy, and C. Khoury, A formal specification of the Steam-Boiler Control problem by algebraic specifications with implicit state, Springer, 1996.
[25] M. Broy, F. Regensburger, B. Schätz, and K. Spies, “Streams of steam–the steam boiler specification case study,” 1998.
[26] P.J. Carreira and M.E. Costa, “Automatically verifying an object- oriented specification of the steam-boiler system,” Proceedings of the 5th International ERCIM Workshop on Formal Methods for In- dustrial Critical Systems (FMICS2000), pp.345–360, 2000.
[27] J.He,“Hybridrelationcalculus,”EngineeringofComplexComputer Systems (ICECCS), 2013 18th International Conference on, pp.2–2, IEEE, 2013.
[28] Y. Yang and X. Li, “Automated enterprise applications generation from requirement model,” CoRR, vol.abs/1609.09656, 2016.
IEICE TRANS. ??, VOL.Exx–??, NO.xx XXXX 200x