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])),