# Automata-Based Analysis of Stage Suspended Boom Systems

Authors: Anping He; Jinzhao Wu; Shihan Yang; Yongquan Zhou; Juan Wang
Journal: Journal of Applied Mathematics
 (2013)

---

## Abstract

A stage suspended boom system is an automatic steeve system orchestrated by the PLC (programmable logic controller). Security and fault-recovering are two important properties. In this paper, we analyze and verify the boom system formally. We adopt the hybrid automaton to model the boom system. The forward reachability is used to verify the properties with the reachable states. We also present a case study to illustrate the feasibility of the proposed verification.


---

## Body

## 1. Introduction

The special effects in live performance make the audience astonishing through colorful background and a stage suspended boom system. Generally, the background indicates a stable scene, but the suspended boom system shows a dynamic stunt. The special effects for live performance are always implemented by suspending objects and/or human in midair from the boom system, such as “little girl flying a kite” in the Olympic Games in Beijing 2008.The contemporary boom systems contain a fixed physical mechanism and a programmable controller, such as the steeve system and PLC. The PLC samples the position of each steeve and restricts their movement periodically. Since human life is at stake, security is the top priority. The boom system is also mission critical due to its live performance nature-stunt. Generally, the stunt is against the security deeply; the audience wants exciting stunts, but actors need safe shows, which makes “Stunt Injuries and Fatalities Increasing” stated by McCann [1].We focus on the formal aspect of analyzing and verifying stage suspended boom systems. The boom system exhibits a hybrid behavior; for example, the continuous behavior in a time period interacts with the discrete events. Therefore, it is natural to adopt hybrid automaton to model and verify this type of system.Hybrid automaton is a formal model for precisely describing hybrid system in which computational processes interact with physical processes. Similar to other types of automaton, the hybrid contains states and transitions, but it also labels and groups relevant dense states as activities to express continuous behaviors, which are described bystate functions. Then the behavior of the hybrid system is composed of discreteness of state transitions and continuity of state evolution.The hybrid automaton was introduced in [2, 3] with analysis for some linear and nonlinear examples, and in [4], the authors focused on its verification aspect. There are many works on verification and analysis of hybrid automata now [4–7] studied the model checking of hybrid automata; [2, 3, 8] performed reachability analysis; [9, 10] studied probabilistic hybrid automata; [11] studied the hybrid automata with a domain-theoretic semantics. Moreover, there are many prior works on the case study of hybrid systems with automata. In [12], the safety properties of the automobile control system are studied. In [9], the hybrid automaton was used to analyze the circuit system. In [10], the authors focused on the sensor-driven hybrid automaton and gave a concrete example of goal network. In [2], an automated manufacturing system is studied. But to the best of our knowledge, no article studies the boom system formally in terms of hybrid automata.In Section2, we show the behaviors of the boom system in a formal way. In Section 3, we analyze a concrete case study for feasibility. We conclude in Section 4.


## 2. Modeling Stage Suspended Boom System

A stage suspended boom system is the system used to achieve a stunt. The contemporary boom system is composed of automatic electromechanical controllers and physical mechanisms, including PLCs, steeves, curtains, and electrical motors. We study this type of system in terms of interactions of steeves and PLCs.


### 2.1. Movement

A boom system performs a stunt by controllable steeves. The steeves are directly driven by electrical motors. We analyze the movement of the system by the movement of steeves. For example, we establish a 4-dimensional mathematical model describing the locus of each steeve, the first 3 dimensions express where the steeve is, and the last one specifies when it arrives there. Letx, y, and z be the first three dimensions and t the last one.The whole movement of steeves is seen as a scene of a boom system. The controllable movement of each steeve is always adjusted and restricted manually or automatically by PLCs. In contemporary boom systems, manual control is only adopted to start a scene or stop it in an emergency. Once the automatic control is triggered, the PLCs manage the movement of steeves continuously unless an emergency occurs.A stunt in a stage provides audience the astonishing effects; at the same time it also provides high risks for an actor/actress. Generally, the inertia and rotation are two main risks while steeves moving. In order to prevent these phenomena, the steeves in a real boom system move slowly and smoothly to reduce inertia; meanwhile, several steel wires connect a steeve and its driver for a consistent movement.For each steeve, it is a mechanical device that behaves under the laws of physics, dealing with quantities of displacement, velocity, and acceleration. The steeve reports its current condition through sensors, adjusts its movement by the reference of actuators, and thus shows a controllable (piecewise) continuous time-variant property. We analyze its behavior by those physics laws.We express the movement of a boom system with the velocity of steeves. To keep the movement slowly and smoothly, the acceleration is really low and close to 0; then in most cases, the velocity is a constant. In addition, the motors in the stage suspended system are commonly constant speed electric ones or the variable-frequency direct-current ones, which makes the control easy and effective. So this type of control belongs to linear ones.Let us show the movement of a steeve. Each steeve of a stage is driven by the electro-motors. Each motor drives a steeve to move forward or backward, left or right, or up or down in terms of a control signal. So the movement of a steeve is a combination of drives of motors. We use the vector and matrix to express the following analysis formally. Let us considerxyz-coordinates of a 3-dimension stage; ui→ be a velocity of the steeve indexed by i, ai a control, fx(xi), fy(yi), and fz(zi) time differential, for example, velocities; axi, ayi, and azi controls; then
(1)ai=(axi000ayi000azi)
and ui→=(fx(xi),fy(yi),fz(zi))×ai. So the movement of the whole boom system, u→, is u→=(u1→,u2→,…,un→). Let a be a control matrix, for example,
(2)a=(a10⋯00a2⋯0⋯00⋯an).
The movement of boom system could be reexpressed as the following:
(3)u→=(fx(x1),fy(y1),fz(z1),fx(x2),fy(y2),fz(z2),…,fx(xn),fy(yn),fz(zn))×a.
Equation (3) shows that the movement of a boom system is depending on the velocity of each motor, for example, velocities in every direction and a control matrix.We call the movement of boom system under a concrete control matrix anactivity, whose number is finite because of the finite number of signals.


### 2.2. Scene

The steeves and the PLCs communicate and cooperate to implement a live performance, for example, a scene.A scene shows the configuration of activities of a boom system in terms of controls from PLCs. Each control is a matrix of concrete control signals, for example, a concrete control value for its movement in a special direction. Letvali be the valuation of a control matrix to a control value matrix. A scene formally defines a sequence of valuations, val1(a),val2(a),…,valk(a),…, that vali(a)≠vali+1(a). We call (vali(a),vali+1(a))   scene related controls.PLCs implement a scene by configuring activities, which construct a hybrid system essentially. For example, the continuous behavior is determined by the steeves, while the discrete one by relation among their movement. The implementation of the scene is complex owing to the nondeterministics of the movement. Steeves driven by motors may not always move functionally, so the PLC owns a mechanism of exceptions.There are two types of nondeterministics: timeout and inconsistency. The timeout indicates that the movement has to finish in a max time duration or the system suspends. The inconsistency involves two phenomena: the inconsistency of the steeve movement in different directions (the motors of a steeve do not cooperate well) or the inconsistency among the moving steeves (the steeves do not cooperate well). All of them have to be treated safely. Let us adjust our scene analysis in terms of these nondeterministics.Let next be a function of getting a next control value matrix with current value. Then for a current control value matrixvali(a), the next may involve three types of matrix: one for the scene requirement, one for the timeout fault, and one(s) for the inconsistent movement.The inconsistency involves source control value matrices, destination matrix, and inconsistent matrix. Let(4)vali(a)=(vi10⋯00vi2⋯0⋯00⋯vin),valj(a)=(vj10⋯00vj2⋯0⋯00⋯vjn),valk(a)=(vk10⋯00vk2⋯0⋯00⋯vkn)
be different controls; for example, not all control signals of motors are the same, ∃l∈{1,…,n} that vil≠vjl≠vkl. We say (vali(a),valk(a),valj(a)) is  processably inconsistent whenever vil=vjl. Then if processable inconsistence holds, vkl=vil and then direction of the movement does not change.Now we can show next control valuation matrix by the scene relation and the processable inconsistency relation. Letnext(val(a))=val′(a) with the following.  (i)
(val(a),val′(a)) is scene related;(ii)
there exists a valuation matrix,vali(a), that (val(a),val′(a),vali(a)) is processably inconsistent, and (val(a),vali(a)) is scene related;(iii)
there exist two activities,vali(a) and valj(a) (i≠j), that (vali(a),valj(a)) is scene related and (val(a),val′(a),valj(a)) and (vali(a),val(a),valj(a)) are processably inconsistent; or(iv)
val′(a) is a suspend control; for example, all control values are 0.


### 2.3. Hybrid Automaton Model

There are several types of definitions for hybrid automata [2–4], all of which construct a position (control model) graph with the events of jump transitions. A hybrid automaton is a sextuple of positions, real-valued variables, event labels, transitions, activities, and invariants. We study the formal model by (forward) reachability analysis; for example, let t, l, and x be a time elapsing, location and variable, and the activity is denoted by ψl[v]. We can verify a hybrid system by the forward analysis of reachability analysis. We compute “time can progress” of max time duration that elapsed in the position l by tcpl[v](t), if for all t1∈[0,t] that  ψl[v](t1)∈Int(l). Then we compute forward time closure of the valuation set of l-position and a special valuation set by v0∈〈P〉ℓ↗, which means ∃v∈V, t∈R≥0 if and only if v∈P∧cpℓ[v](t)∧v0=ψℓ[v](t). And then we compute postcondition of a set of valuations generated through transitions by v1∈poste[P], which means ∃v∈V if and only if v∈P∧(v,v1)∈μ. So finally we compute the set of reachable states by the fixpoint of the following equation:  (5)Xℓ=〈Iℓ⋃e=(ℓ0,ℓ)∈Edg‍poste[Xℓ0]〉ℓ↗
with I=⋃ℓ∈Loc‍(ℓ,Iℓ) being a set of initial states.The (piecewise) continuous movement (see Section2.1) builds the part of (piecewise) continuous behavior of a boom system. In contrast, periodically and discretely, the PLC implements a scene of live performance, by monitoring the continuous behavior (by sensors), generating decisions (by logic reasoning and data processing programs), and then writes the compatible controls into the actuators, instantaneously. The control may change the system movement by adding the boom system discrete behaviors (see Section 2.2). In short, the interacted (piecewise) continuity and discreteness of this system present a hybrid behavior, indeed.It is very convenient to translate the analysis in previous subsections into a hybrid automaton. The variables include all movement variables, signal variables, and other special ones; the locations, as well as activities contained in the location, are corresponding to the activities of system movement directly; the edges between the activities are described by the next function; the invariant of each location involves the max time allowed for every activity, which is concluded from scene. We will show the hybrid automaton in the following case study.


## 2.1. Movement

A boom system performs a stunt by controllable steeves. The steeves are directly driven by electrical motors. We analyze the movement of the system by the movement of steeves. For example, we establish a 4-dimensional mathematical model describing the locus of each steeve, the first 3 dimensions express where the steeve is, and the last one specifies when it arrives there. Letx, y, and z be the first three dimensions and t the last one.The whole movement of steeves is seen as a scene of a boom system. The controllable movement of each steeve is always adjusted and restricted manually or automatically by PLCs. In contemporary boom systems, manual control is only adopted to start a scene or stop it in an emergency. Once the automatic control is triggered, the PLCs manage the movement of steeves continuously unless an emergency occurs.A stunt in a stage provides audience the astonishing effects; at the same time it also provides high risks for an actor/actress. Generally, the inertia and rotation are two main risks while steeves moving. In order to prevent these phenomena, the steeves in a real boom system move slowly and smoothly to reduce inertia; meanwhile, several steel wires connect a steeve and its driver for a consistent movement.For each steeve, it is a mechanical device that behaves under the laws of physics, dealing with quantities of displacement, velocity, and acceleration. The steeve reports its current condition through sensors, adjusts its movement by the reference of actuators, and thus shows a controllable (piecewise) continuous time-variant property. We analyze its behavior by those physics laws.We express the movement of a boom system with the velocity of steeves. To keep the movement slowly and smoothly, the acceleration is really low and close to 0; then in most cases, the velocity is a constant. In addition, the motors in the stage suspended system are commonly constant speed electric ones or the variable-frequency direct-current ones, which makes the control easy and effective. So this type of control belongs to linear ones.Let us show the movement of a steeve. Each steeve of a stage is driven by the electro-motors. Each motor drives a steeve to move forward or backward, left or right, or up or down in terms of a control signal. So the movement of a steeve is a combination of drives of motors. We use the vector and matrix to express the following analysis formally. Let us considerxyz-coordinates of a 3-dimension stage; ui→ be a velocity of the steeve indexed by i, ai a control, fx(xi), fy(yi), and fz(zi) time differential, for example, velocities; axi, ayi, and azi controls; then
(1)ai=(axi000ayi000azi)
and ui→=(fx(xi),fy(yi),fz(zi))×ai. So the movement of the whole boom system, u→, is u→=(u1→,u2→,…,un→). Let a be a control matrix, for example,
(2)a=(a10⋯00a2⋯0⋯00⋯an).
The movement of boom system could be reexpressed as the following:
(3)u→=(fx(x1),fy(y1),fz(z1),fx(x2),fy(y2),fz(z2),…,fx(xn),fy(yn),fz(zn))×a.
Equation (3) shows that the movement of a boom system is depending on the velocity of each motor, for example, velocities in every direction and a control matrix.We call the movement of boom system under a concrete control matrix anactivity, whose number is finite because of the finite number of signals.


## 2.2. Scene

The steeves and the PLCs communicate and cooperate to implement a live performance, for example, a scene.A scene shows the configuration of activities of a boom system in terms of controls from PLCs. Each control is a matrix of concrete control signals, for example, a concrete control value for its movement in a special direction. Letvali be the valuation of a control matrix to a control value matrix. A scene formally defines a sequence of valuations, val1(a),val2(a),…,valk(a),…, that vali(a)≠vali+1(a). We call (vali(a),vali+1(a))   scene related controls.PLCs implement a scene by configuring activities, which construct a hybrid system essentially. For example, the continuous behavior is determined by the steeves, while the discrete one by relation among their movement. The implementation of the scene is complex owing to the nondeterministics of the movement. Steeves driven by motors may not always move functionally, so the PLC owns a mechanism of exceptions.There are two types of nondeterministics: timeout and inconsistency. The timeout indicates that the movement has to finish in a max time duration or the system suspends. The inconsistency involves two phenomena: the inconsistency of the steeve movement in different directions (the motors of a steeve do not cooperate well) or the inconsistency among the moving steeves (the steeves do not cooperate well). All of them have to be treated safely. Let us adjust our scene analysis in terms of these nondeterministics.Let next be a function of getting a next control value matrix with current value. Then for a current control value matrixvali(a), the next may involve three types of matrix: one for the scene requirement, one for the timeout fault, and one(s) for the inconsistent movement.The inconsistency involves source control value matrices, destination matrix, and inconsistent matrix. Let(4)vali(a)=(vi10⋯00vi2⋯0⋯00⋯vin),valj(a)=(vj10⋯00vj2⋯0⋯00⋯vjn),valk(a)=(vk10⋯00vk2⋯0⋯00⋯vkn)
be different controls; for example, not all control signals of motors are the same, ∃l∈{1,…,n} that vil≠vjl≠vkl. We say (vali(a),valk(a),valj(a)) is  processably inconsistent whenever vil=vjl. Then if processable inconsistence holds, vkl=vil and then direction of the movement does not change.Now we can show next control valuation matrix by the scene relation and the processable inconsistency relation. Letnext(val(a))=val′(a) with the following.  (i)
(val(a),val′(a)) is scene related;(ii)
there exists a valuation matrix,vali(a), that (val(a),val′(a),vali(a)) is processably inconsistent, and (val(a),vali(a)) is scene related;(iii)
there exist two activities,vali(a) and valj(a) (i≠j), that (vali(a),valj(a)) is scene related and (val(a),val′(a),valj(a)) and (vali(a),val(a),valj(a)) are processably inconsistent; or(iv)
val′(a) is a suspend control; for example, all control values are 0.


## 2.3. Hybrid Automaton Model

There are several types of definitions for hybrid automata [2–4], all of which construct a position (control model) graph with the events of jump transitions. A hybrid automaton is a sextuple of positions, real-valued variables, event labels, transitions, activities, and invariants. We study the formal model by (forward) reachability analysis; for example, let t, l, and x be a time elapsing, location and variable, and the activity is denoted by ψl[v]. We can verify a hybrid system by the forward analysis of reachability analysis. We compute “time can progress” of max time duration that elapsed in the position l by tcpl[v](t), if for all t1∈[0,t] that  ψl[v](t1)∈Int(l). Then we compute forward time closure of the valuation set of l-position and a special valuation set by v0∈〈P〉ℓ↗, which means ∃v∈V, t∈R≥0 if and only if v∈P∧cpℓ[v](t)∧v0=ψℓ[v](t). And then we compute postcondition of a set of valuations generated through transitions by v1∈poste[P], which means ∃v∈V if and only if v∈P∧(v,v1)∈μ. So finally we compute the set of reachable states by the fixpoint of the following equation:  (5)Xℓ=〈Iℓ⋃e=(ℓ0,ℓ)∈Edg‍poste[Xℓ0]〉ℓ↗
with I=⋃ℓ∈Loc‍(ℓ,Iℓ) being a set of initial states.The (piecewise) continuous movement (see Section2.1) builds the part of (piecewise) continuous behavior of a boom system. In contrast, periodically and discretely, the PLC implements a scene of live performance, by monitoring the continuous behavior (by sensors), generating decisions (by logic reasoning and data processing programs), and then writes the compatible controls into the actuators, instantaneously. The control may change the system movement by adding the boom system discrete behaviors (see Section 2.2). In short, the interacted (piecewise) continuity and discreteness of this system present a hybrid behavior, indeed.It is very convenient to translate the analysis in previous subsections into a hybrid automaton. The variables include all movement variables, signal variables, and other special ones; the locations, as well as activities contained in the location, are corresponding to the activities of system movement directly; the edges between the activities are described by the next function; the invariant of each location involves the max time allowed for every activity, which is concluded from scene. We will show the hybrid automaton in the following case study.


## 3. A Case Study

For this specific boom system, each steeve is driven by two constant speed electric motors located in vertical and horizontal directions. A moving steeve could be stopped at any position if a stop button is pushed for some security reasons; moreover, after the operator pushes the start button, each steeve moves automatically under the control of the PLCs. The PLCs are used as intelligent controllers. The electric motor rotates in a constant speed to keep the steeve moving placidly. The transducers fixed on motors will send 256 pulses per motor rotation cycle, and the steeve will move 16cm. The PLCs memorize and calculate the number of pulses to control the electric motor. Moreover, the direction of motor rotation can be adjusted to move down (or left) or to up (or right) by the PLC signals.We study an interesting scene, for example, a stunt thata actor/actress riding a bicycle to climb “hill”, the bicycle is hung on a steeve in a xy coordination. Initially, the bicycle locates at the (0,0) position, then the bicycle, as well as the actor, begins to climbing a hill, for example, moves slowly to position (L,H), and then (0,2×H) of the top of the hill. Then the bicycle moves from one peak to another horizontally. And then moves down the hill and arrives at foot (L,0). Finally, moves to the initial position (0,0) and begins to another cycle.We consider the following problems.(i)
Does the state suspended boom system perform safely?(ii)
Does the state suspended boom system perform correctly?


### 3.1. Hybrid Automata

We have two button-related variables: start and stop for start and stop stunt manually. The scene of this case study involves one steeve and one PLC and plays a 2D movement. So we get two movement related variables:x and y for x-axis and y-axis. The PLC samples the movement indirectly; it records and calculates the pulse number of each angular transducer of motors. Then two special variables are necessary, let xc be pulse counter for x-axis moving, and yc for the other. Moreover, we use another variable for local timer, for example, let d record the elapsed time of a position (or control model). Then the variable set is Var={start,stop,x,y,xc,yc,d}, and controlled variable set Con={x,y,xc,yc,d}.Letvx and vy be constants for velocities of the steeve in x and y directions separately. Only one steeve be used in this scene; the movement is expressed by velocities and rates of pulse; so by the way introduced in Section 2, we get  a=(ax00ay)  and u→=(vx,vy)×a.According to the specification, the controlax (ay) makes a steeve moving left or right (up or down); so we set its value as {-1,0,1} for moving left, stopping moving, and right (similar to ay). Then we get the nine activities in Table 1 with (3).Table 1
The activities.
a
u
Up-right
va
l
ur
(
a
)
=
(
1
0
0
1
)
u
ur
=
(
v
x
,
v
y
)
Up-left
va
l
ul
(
a
)
=
(
-
1
0
0
1
)
u
ur
=
(
-
v
x
,
v
y
)
Down-left
va
l
ur
(
a
)
=
(
-
1
0
0
-
1
)
u
dl
=
(
-
v
x
,
-
v
y
)
Down-right
va
l
ur
(
a
)
=
(
1
0
0
-
1
)
u
dr
=
(
v
x
,
-
v
y
)
Up
va
l
ur
(
a
)
=
(
0
0
0
1
)
u
u
=
(
0
,
v
y
)
Down
va
l
ur
(
a
)
=
(
0
0
0
-
1
)
u
d
=
(
0
,
-
v
y
)
Right
va
l
ur
(
a
)
=
(
1
0
0
0
)
u
r
=
(
v
x
,
0
)
Left
va
l
ur
(
a
)
=
(
-
1
0
0
0
)
u
l
=
(
-
v
x
,
0
)
Suspend
va
l
ur
(
a
)
=
(
0
0
0
0
)
u
sp
=
(
0,0
)The scene defines a sequence of controls:valur(a), valul(a), valr(a), valdl(a), valdr(a), and vall(a). We extend this control sequence by consistency and timeout analysis; let us take a scene relation (valur(a),valul(a)) as an example,  (6)next(valur(a))=next((1001))={(0000),(0001),(1000)}.So when the steeve is moving up-right, it may suspend for timeout, or its horizontal/vertical movement finishes but the vertical/horizontal not (see the shadow in Figure1). In this figure, the x-position movement finishes in t1 time point; the y-direction displacement of any (red) line in the shadow is necessary for the consistency. After calculating all the next control valuation matrixes, we get the connected graph in Figure 2 without formulas.Figure 1
The fault self-recovered movement.Figure 2
The hybrid automaton of riding a bicycle.PLC cannot add more movement of boom system but only can organize some activities to form a scene; so as we talked in Section2.3, we can build the hybrid automaton according to the patterns of movement, for example,
(7)Loc={ur,ul,dl,dr,up,down,right,left,susp}.
We write ur as up-right for short;  others are similar. The Act of a location is the same as the corresponding activity previously.The PLC reads transducer sensors to adjust movement of a steeve to implement the stunt, the rate of pulse of a sensor is the same as the velocity of a steeve, and it is convenient to show the invariant and edges by pulse counterxc and yc. Let us define hypothesis to make the following expression simple. Let NL and NH be two pulse constants with NL=(256/16)×L=16×L and NH=16×H; let int returns the integer portion of a number and mod be a function of getting the remainder produced by being divided into two integers. We define the following assertions:  (8)stop∶=start=0∧stop=1,auto∶=start=1∧stop=0,hmv∶=mod(int(xc),NL)≤NL,vmv∶=mod(int(yc),NH)≤NH,hslp∶=mod(int(xc),NL)=0,vslp∶=mod(int(yc),NH)=0,D∶=d≤Tmax,
where stop and auto are two assertions for the steeve suspending and moving automatically, hmv and vmv for moving horizontally and vertically, hslp and vslp for sleeping on horizontal or vertical directions,  and the last one D for the max time duration of a movement. Then the Inv of each location will be (9)Inv(ur)∶=Inv(ul)∶=Inv(dl)∶=Inv(dr)∶=hmv∧vmv∧D∧auto,Inv(up)∶=Inv(down)∶=hslp∧vmv∧D∧auto,Inv(right)∶=Inv(left)∶=hmv∧vslp∧D∧auto,Inv(susp)∶=stop.We getEdg from the next function, which defines the transition among control valuation matrixes. According to the definition of next(valur)), we know the next location of up-right ur will be up, susp, and right as seen in Table 1. Let us show an example of the transition from ur to up. In each cycle, the moving distance on x-axis is 6×L that the direction of the displacement changes once increasing L and so is the movement along the y-axis. The ur to up transition happens to recover the moving error when the up-right movement of scene performs; for example, if the movement on x-axis finishes before the one on y-axis, the bicycle moves up-right, then up, and finally up-left; then the condition of the jump shows the finish of the first x-axis movement, for example, the 6k×L+L distance. So we get the following formulae:
(10)μ:=mod(int(xc)÷NL,6)=1∧mode(int(xc),NL)=0.
Then the transition expression is e=(ur,α,μ,up) in which  α is an event label.Step by step, we construct a hybrid automaton in Figure2 (each position is indexed by an integer number for utility).


### 3.2. Reachability Analysis

We can prove some interesting properties by reachability analysis of the hybrid automaton in Figure2. Let us use the forward analysis method in Section 2.3 to compute reachable state set from initial states.The initial states illustrate that the steeve starts moving up-right from the coordination(0,0); meanwhile, the elapsed time begins to be recorded. Let pc be an integer over indexes of positions; we express the initial states as a formula ψI:
(11)ψI∶=pc=1∧x=y=xc=yc=d=0∧start=1∧stop=0.According to (5), the reachable states are characterized by the least fixpoint of the following nine equations:
(12)ψ1=〈ψI1∨post(8,1)[ψ8]〉1↗,ψ2=〈ψI2∨post(1,2)[ψ1]∨post(3,2)[ψ3]〉2↗,ψ3=〈ψI3∨post(2,3)[ψ2]∨post(4,3)[ψ4]〉3↗,ψ4=〈ψI4∨post(1,4)[ψ1]∨post(2,4)[ψ2]∨post(7,4)[ψ7]∨post(8,4)[ψ8]〉4↗,ψ5=〈ψI5∨post(4,5)[ψ4]〉5↗,ψ6=〈ψI6∨post(5,6)[ψ5]∨post(7,6)[ψ7]〉6↗,ψ7=〈ψI7∨post(6,7)[ψ6]∨post(8,7)[ψ8]〉7↗,ψ8=〈ψI8∨post(3,8)[ψ3]∨post(4,8)[ψ4]∨post(5,8)[ψ5]∨post(6,8)[ψ6]〉8↗,ψ9=〈ψI9∨post(1,9)[ψ1]∨post(2,9)[ψ2]∨post(3,9)[ψ3]∨post(4,9)[ψ4]∨post(5,9)[ψ5]∨post(6,9)[ψ6]∨post(7,9)[ψ7]∨post(8,9)[ψ8]〉9↗.By the initial states,ψI1=ψI and ψI2=⋯=ψI9=false, we can calculate the fixpoint of (12) iteratively, for example, let i=1,2,… be the times iterated; we calculate the first equation by ψ1,i=〈ψ1,i-1∨post(8,1)[ψ8,i-1]〉1↗; then we get
(13)ψ1=(0≤x≤L∧0≤y≤H∧6×C1≤xc≤6×C1+NL∧4×C2≤yc≤4×C2+NH∧D∧auto)
with k=1,2,3,… being the number of cycles of movement, C1=(k-1)×NL, C2=(k-1)×NH, and so are the others.The safety properties can be studied in terms of the reachable states. We list properties as the lemmas bellow.Lemma 1.
After a scene begins to perform, the movement of the boom system will be in a safe area, for example, a rectangle of(0,0),(0,L),(L,2×H),and(0,2×H):
(14)t≥0⇒0≤x≤L∧0≤y≤2×H.Lemma 2.
In each activity, if duration of the activity is longer thanTmax, the movement will stop, for example.
(15)t>Tmax⇒ψ9.These two security properties are direct from the reachable states.Lemma 3.
The behavior of the system conforms to the specification of the scene.Proof.
This lemma requires that the movement of steeves follows the scene specification; for example, implementation of the bicycle climbing the hill-zigzag traces appears once duration resetting transition (d:=0) is triggered. For example, if the steeve arrives at the position (L,H) (the PLC controller only knows this from xc=6×k×NL+NL∧yc=4×k×NH+NH with k being the number of cycles of movement), a zigzag appears, for example,
(16)xc=6k×NL+NL∧yc=4k×NH+NH⇒(((6k×NL≤xc<6k×NL+NL)∧(4k×NH<yc<4k×NH+NH)∧(0≤x<L∧0≤y<H))∨(x=L∧y=H))∨((6k×NL+NL≤xc<6k×NL+2×NL)∧(4k×NH+NHyc<4k×NH+2×NH)∧(0≤x<L∧H<y≤2×H)).
The formula xc=6×k×NL+NL∧yc=4×k×NH+NH implies that ψ1, ψ2, ψ3, ψ4, and ψ9 hold. Then we can check that the set of states characterized by the formulas after ⇒ is a subset of states defined by (ψ1∨ψ2∨ψ3∨ψ4∨ψ9). The formal specifications and proofs of other zigzag trace, are similar. So we know that the hybrid system of the boom system holds the specification of the scene, and then lemma 3 is proved.Lemma 4.
The boom system recovers its fault movement by itself.Proof.
Let us take the zigzag trace for example, if the time duration of the up-right movement is less thanTmax and the x-direction movement finishes but y-direction movement not, then x-direction movement stops and waits for the y-direction movement, for example,
(17)(t≤Tmax∧xc=6×k×NL+NL∧yc<4×k×NH+NH∧start=1∧stop=0)⇒ψ2.
The proof can be directly reasoned from the formulas of reachable states. Similarly, we can verify other fault-recovering requirements by their characterization of the reachable states.


## 3.1. Hybrid Automata

We have two button-related variables: start and stop for start and stop stunt manually. The scene of this case study involves one steeve and one PLC and plays a 2D movement. So we get two movement related variables:x and y for x-axis and y-axis. The PLC samples the movement indirectly; it records and calculates the pulse number of each angular transducer of motors. Then two special variables are necessary, let xc be pulse counter for x-axis moving, and yc for the other. Moreover, we use another variable for local timer, for example, let d record the elapsed time of a position (or control model). Then the variable set is Var={start,stop,x,y,xc,yc,d}, and controlled variable set Con={x,y,xc,yc,d}.Letvx and vy be constants for velocities of the steeve in x and y directions separately. Only one steeve be used in this scene; the movement is expressed by velocities and rates of pulse; so by the way introduced in Section 2, we get  a=(ax00ay)  and u→=(vx,vy)×a.According to the specification, the controlax (ay) makes a steeve moving left or right (up or down); so we set its value as {-1,0,1} for moving left, stopping moving, and right (similar to ay). Then we get the nine activities in Table 1 with (3).Table 1
The activities.
a
u
Up-right
va
l
ur
(
a
)
=
(
1
0
0
1
)
u
ur
=
(
v
x
,
v
y
)
Up-left
va
l
ul
(
a
)
=
(
-
1
0
0
1
)
u
ur
=
(
-
v
x
,
v
y
)
Down-left
va
l
ur
(
a
)
=
(
-
1
0
0
-
1
)
u
dl
=
(
-
v
x
,
-
v
y
)
Down-right
va
l
ur
(
a
)
=
(
1
0
0
-
1
)
u
dr
=
(
v
x
,
-
v
y
)
Up
va
l
ur
(
a
)
=
(
0
0
0
1
)
u
u
=
(
0
,
v
y
)
Down
va
l
ur
(
a
)
=
(
0
0
0
-
1
)
u
d
=
(
0
,
-
v
y
)
Right
va
l
ur
(
a
)
=
(
1
0
0
0
)
u
r
=
(
v
x
,
0
)
Left
va
l
ur
(
a
)
=
(
-
1
0
0
0
)
u
l
=
(
-
v
x
,
0
)
Suspend
va
l
ur
(
a
)
=
(
0
0
0
0
)
u
sp
=
(
0,0
)The scene defines a sequence of controls:valur(a), valul(a), valr(a), valdl(a), valdr(a), and vall(a). We extend this control sequence by consistency and timeout analysis; let us take a scene relation (valur(a),valul(a)) as an example,  (6)next(valur(a))=next((1001))={(0000),(0001),(1000)}.So when the steeve is moving up-right, it may suspend for timeout, or its horizontal/vertical movement finishes but the vertical/horizontal not (see the shadow in Figure1). In this figure, the x-position movement finishes in t1 time point; the y-direction displacement of any (red) line in the shadow is necessary for the consistency. After calculating all the next control valuation matrixes, we get the connected graph in Figure 2 without formulas.Figure 1
The fault self-recovered movement.Figure 2
The hybrid automaton of riding a bicycle.PLC cannot add more movement of boom system but only can organize some activities to form a scene; so as we talked in Section2.3, we can build the hybrid automaton according to the patterns of movement, for example,
(7)Loc={ur,ul,dl,dr,up,down,right,left,susp}.
We write ur as up-right for short;  others are similar. The Act of a location is the same as the corresponding activity previously.The PLC reads transducer sensors to adjust movement of a steeve to implement the stunt, the rate of pulse of a sensor is the same as the velocity of a steeve, and it is convenient to show the invariant and edges by pulse counterxc and yc. Let us define hypothesis to make the following expression simple. Let NL and NH be two pulse constants with NL=(256/16)×L=16×L and NH=16×H; let int returns the integer portion of a number and mod be a function of getting the remainder produced by being divided into two integers. We define the following assertions:  (8)stop∶=start=0∧stop=1,auto∶=start=1∧stop=0,hmv∶=mod(int(xc),NL)≤NL,vmv∶=mod(int(yc),NH)≤NH,hslp∶=mod(int(xc),NL)=0,vslp∶=mod(int(yc),NH)=0,D∶=d≤Tmax,
where stop and auto are two assertions for the steeve suspending and moving automatically, hmv and vmv for moving horizontally and vertically, hslp and vslp for sleeping on horizontal or vertical directions,  and the last one D for the max time duration of a movement. Then the Inv of each location will be (9)Inv(ur)∶=Inv(ul)∶=Inv(dl)∶=Inv(dr)∶=hmv∧vmv∧D∧auto,Inv(up)∶=Inv(down)∶=hslp∧vmv∧D∧auto,Inv(right)∶=Inv(left)∶=hmv∧vslp∧D∧auto,Inv(susp)∶=stop.We getEdg from the next function, which defines the transition among control valuation matrixes. According to the definition of next(valur)), we know the next location of up-right ur will be up, susp, and right as seen in Table 1. Let us show an example of the transition from ur to up. In each cycle, the moving distance on x-axis is 6×L that the direction of the displacement changes once increasing L and so is the movement along the y-axis. The ur to up transition happens to recover the moving error when the up-right movement of scene performs; for example, if the movement on x-axis finishes before the one on y-axis, the bicycle moves up-right, then up, and finally up-left; then the condition of the jump shows the finish of the first x-axis movement, for example, the 6k×L+L distance. So we get the following formulae:
(10)μ:=mod(int(xc)÷NL,6)=1∧mode(int(xc),NL)=0.
Then the transition expression is e=(ur,α,μ,up) in which  α is an event label.Step by step, we construct a hybrid automaton in Figure2 (each position is indexed by an integer number for utility).


## 3.2. Reachability Analysis

We can prove some interesting properties by reachability analysis of the hybrid automaton in Figure2. Let us use the forward analysis method in Section 2.3 to compute reachable state set from initial states.The initial states illustrate that the steeve starts moving up-right from the coordination(0,0); meanwhile, the elapsed time begins to be recorded. Let pc be an integer over indexes of positions; we express the initial states as a formula ψI:
(11)ψI∶=pc=1∧x=y=xc=yc=d=0∧start=1∧stop=0.According to (5), the reachable states are characterized by the least fixpoint of the following nine equations:
(12)ψ1=〈ψI1∨post(8,1)[ψ8]〉1↗,ψ2=〈ψI2∨post(1,2)[ψ1]∨post(3,2)[ψ3]〉2↗,ψ3=〈ψI3∨post(2,3)[ψ2]∨post(4,3)[ψ4]〉3↗,ψ4=〈ψI4∨post(1,4)[ψ1]∨post(2,4)[ψ2]∨post(7,4)[ψ7]∨post(8,4)[ψ8]〉4↗,ψ5=〈ψI5∨post(4,5)[ψ4]〉5↗,ψ6=〈ψI6∨post(5,6)[ψ5]∨post(7,6)[ψ7]〉6↗,ψ7=〈ψI7∨post(6,7)[ψ6]∨post(8,7)[ψ8]〉7↗,ψ8=〈ψI8∨post(3,8)[ψ3]∨post(4,8)[ψ4]∨post(5,8)[ψ5]∨post(6,8)[ψ6]〉8↗,ψ9=〈ψI9∨post(1,9)[ψ1]∨post(2,9)[ψ2]∨post(3,9)[ψ3]∨post(4,9)[ψ4]∨post(5,9)[ψ5]∨post(6,9)[ψ6]∨post(7,9)[ψ7]∨post(8,9)[ψ8]〉9↗.By the initial states,ψI1=ψI and ψI2=⋯=ψI9=false, we can calculate the fixpoint of (12) iteratively, for example, let i=1,2,… be the times iterated; we calculate the first equation by ψ1,i=〈ψ1,i-1∨post(8,1)[ψ8,i-1]〉1↗; then we get
(13)ψ1=(0≤x≤L∧0≤y≤H∧6×C1≤xc≤6×C1+NL∧4×C2≤yc≤4×C2+NH∧D∧auto)
with k=1,2,3,… being the number of cycles of movement, C1=(k-1)×NL, C2=(k-1)×NH, and so are the others.The safety properties can be studied in terms of the reachable states. We list properties as the lemmas bellow.Lemma 1.
After a scene begins to perform, the movement of the boom system will be in a safe area, for example, a rectangle of(0,0),(0,L),(L,2×H),and(0,2×H):
(14)t≥0⇒0≤x≤L∧0≤y≤2×H.Lemma 2.
In each activity, if duration of the activity is longer thanTmax, the movement will stop, for example.
(15)t>Tmax⇒ψ9.These two security properties are direct from the reachable states.Lemma 3.
The behavior of the system conforms to the specification of the scene.Proof.
This lemma requires that the movement of steeves follows the scene specification; for example, implementation of the bicycle climbing the hill-zigzag traces appears once duration resetting transition (d:=0) is triggered. For example, if the steeve arrives at the position (L,H) (the PLC controller only knows this from xc=6×k×NL+NL∧yc=4×k×NH+NH with k being the number of cycles of movement), a zigzag appears, for example,
(16)xc=6k×NL+NL∧yc=4k×NH+NH⇒(((6k×NL≤xc<6k×NL+NL)∧(4k×NH<yc<4k×NH+NH)∧(0≤x<L∧0≤y<H))∨(x=L∧y=H))∨((6k×NL+NL≤xc<6k×NL+2×NL)∧(4k×NH+NHyc<4k×NH+2×NH)∧(0≤x<L∧H<y≤2×H)).
The formula xc=6×k×NL+NL∧yc=4×k×NH+NH implies that ψ1, ψ2, ψ3, ψ4, and ψ9 hold. Then we can check that the set of states characterized by the formulas after ⇒ is a subset of states defined by (ψ1∨ψ2∨ψ3∨ψ4∨ψ9). The formal specifications and proofs of other zigzag trace, are similar. So we know that the hybrid system of the boom system holds the specification of the scene, and then lemma 3 is proved.Lemma 4.
The boom system recovers its fault movement by itself.Proof.
Let us take the zigzag trace for example, if the time duration of the up-right movement is less thanTmax and the x-direction movement finishes but y-direction movement not, then x-direction movement stops and waits for the y-direction movement, for example,
(17)(t≤Tmax∧xc=6×k×NL+NL∧yc<4×k×NH+NH∧start=1∧stop=0)⇒ψ2.
The proof can be directly reasoned from the formulas of reachable states. Similarly, we can verify other fault-recovering requirements by their characterization of the reachable states.


## 4. Conclusion

In this paper, we adopted hybrid automaton as the model of the boom system, and then used the forward method to analyze its reachability problem. Some important properties were verified in terms of the reachable states. An interesting case study of scene of bicycle climbing hill was shown to prove the feasibility of our study.In future, we will adopt tools of hybrid automata to make the analysis and verification (possibly) automatically. After many case studies, we regard there could be a framework of modeling and verifying this type of system; so we will study more cases to find their characteristics, and then propose a practice framework (which may not only be solvable by hybrid automata).



---

*Source: 739253-2013-03-31.xml*