Verification of Safety Property of Line Tracer Programusing Timed Automaton Model
Kozo Okano† , Toshifusa Sekizawa‡ , Hiroaki Shimba† , Hideki Kawai‡ , Kentaro Hanada† ,Yukihiro Sasaki† , and Shinji Kusumoto††

Graduate School of Information Science and Techlology, Osaka University, Japan‡
Faculty of Informatics, Osaka Gakuin University, Japan{okano, h-shimba, k-hanada,y-sasaki, kusumoto}@ist.osaka-u.ac.jp{sekizawa,09s0100}@ogu.ac.jp
reported, including verification of audio-video protocols[3],a gear controller[4], timeliness properties of multimedia systems [5], and so on.
Embedded systems sometimes control continuous systems.
For examples, water level controller observes level of waterin a certain water tank and controls incoming and outgoingvalve flow associated with the tank. Note that the water level
and the valve flow are usually continuous values. In orderto deal with such a system consisting of discrete sub-systems
and continuous sub-systems, hybrid automaton has been also
proposed. Several studies have proposed simulators for hybrid systems.
Our research question is how to verify formally behavior ofsuch hybrid systems[6]. Our first step of the research is to findwhat properties can be verified using conventional verifiers
such as UPPAAL and so on, through a real application. We
use a line tracer as a real application for the following reasons.

Abstract - Recently reliability of embedded systems has
become very important. Such reliability can be ensured byformal verification techniques including model checking. We
study such verification technique through a real example ofembedded systems, a line tracer. This paper mainly describes
how to model the behavior of the line tracer in a network of
timed automata, as well as experimental results of verification. Using the model, several safety properties are successfully verified with a model checker, UPPAAL. The line tracer
is built with LEGO Mindstorms kit. This paper also describes
the implementation using LeJOS, a Java development environment for LEGO Mindstorms kit.
Keywords: Embedded System, Real-time System, Formal
Verification, Timed Automaton

1

INTRODUCTION• It contains time properties as design specification;

Recently, embedded systems have become important in oursociety. Embedded systems exist everywhere in our daily
life. Therefore, to ensure safety properties of the embedded
systems becomes much important. In order to ensure suchproperty, model checking techniques are often used. Most ofmodel checking techniques are based on finite state machinemodel. The behavior of the target systems is modeled in a tuple of automata. In usual, program variables, such as integer
variables are translated into finite state variables. For example, a general 32-bit integer variable might be translated into
an 8-bit integer as long as the target program does not use constants with large values greater than 127. Even such modeling can detect important faults in design phases. On the other
hand, some of embedded systems require time properties as
their specification. In order to model such systems (real-timesystems), several models have been proposed. Timed automaton is proposed by Alur and Dill[1]. The most interesting
point of timed automaton is that it uses clock variables where
the range of a clock variable is real numbers. Locations andtransitions of timed automaton have constraints on clocks inlimited syntax forms. Timed automaton, therefore, can represent naturally behavior of real-time systems. The famous verifier for timed automaton is UPPAAL[2], which is developedby Wang-Yi’s research group. The timed automaton used in
UPPAAL is a strong extension of the original timed automaton. It can deal with bounded integer variables and guard expressions on its transitions can express constraints on suchvariables. Several success applications of verification have

• We can implement a real system with reasonable costs
using LEGO Mindstorms kit [7]; and• We can freely describe the control program in Java using LeJOS[8], which is free software for LEGO Mindstorms.
Through experiments, we have succeeded in verificationof safety properties of a line tracer, using timed automaton
model and UPPAAL.
The rest of the paper is organized as follows. Sec. 2 provides preliminaries. Sec. 3 and 4 will describe the model andimplementation of our line tracer. Sec.5 and 6 show somepreliminary but promise experiments and discussion. Finally,
Sec. 7 concludes the paper. The final section also provides
future plan of our work.

2 PRELIMINARIES
Here, we will provide several definitions and notions usedin this paper.

2.1 Timed Automaton
A timed automaton is an extension of the conventional automaton with clock variables and constraints for expressing
real-time dynamics. They are widely used in the modelingand analysis of real-time systems.

136

a,g,rl1 → l2 , g(v), I(l2 )(r(v))

Definition 1 (constraints) We use the following constraints
on clocks.

a(l1 , v) ⇒ (l2 , r(v))

1. C represents a finite set of clocks.

,∀d" ≤ d I(l1 )(v + d" )d(l1 , v) ⇒ (l1 , v + d)

Semantics of a timed automaton can be interpreted as a labeled transition system.

2. Constraints c(C) over clocks C are expressed as inequality of the following form.

Definition 4 (semantic of a timed automaton) For a timed
automaton A = (A, L, l 0 , C, T, I), an infinite transition system is defined according to the semantics of A , where theαmodel begins with the initial state. By T (A ) = (S, s 0 , ⇒),the semantic model of A is denoted, where α ∈ A ∪ R ≥0 .

E ::= x ∼ a | x − y ∼ b | E1 ∧ E2 ,where x, y ∈ C, ∼∈ {≤, ≥, <, >, =}, and a, b ∈ R≥0 ,in which R≥0 , is a set of all non-negative real numbers.
The above time constraints are used to mark edges andnodes of the timed automata for describing the guards andinvariants.

Definition 5 (run of a timed automaton) For a timed automaton A , a run σ is finite or infinite sequence of transitions ofT (A ).
ααα
σ = (l0 , ν0 ) ⇒1 (l1 , ν1 ) ⇒2 (l2 , ν2 ) ⇒3 · · ·Definition 2 (timed automaton) A timed automaton A is a
6-tuple (A, L, l0 , C, T, I), where

2.2 UPPAALUPPAAL[2] is a famous model checker for extended timed
automata by Wang-Yi et al. It also supports model checking
for the conventional timed automata. UPPAAL allows verification of expressions described in an extended version of
CTL. In addition, it supports local and global integers andprimitive operations on integers, such as addition, subtract
and multiplication with constants. Such expressions are also
allowed on the guards of transitions. The model of the system can be created from multiple timed automata which aresynchronized together via CCS-like synchronization mechanisms.
The important point is that even the extended timed automaton used in UPPAAL cannot deal with real variables except clocks. We, therefore, have to round real values to integer
values when we model the target systems.

• A: a finite set of actions;• L: a finite set of locations;• l0 ∈ L: an initial location;• C: a finite set of clocks;• T ⊆ L × c(C) × A × 2C × L is a set of transitions. The
second and fourth items are called a guard and clock
resets, respectively; and• I : L → c(C) is a mapping from location to clock
constraints, called a location invariant.
a,g,r

l2 .

A transition t = (l1 , g, a, r, l2 ) ∈ T is denoted by l 1 →3 MODELA map v : C → R≥0 , is called a clock assignment (or clock
valuation). We define (v + d)(x) = v(x) + d for d ∈ R ≥0and some x ∈ C.
For a guard, a reset and a location invariant, we introduce
some notations with regard to clock valuation. For each guardg ∈ c(C), a function g(v) stands for the valuation of theguard expression g with the clock valuation v. For each reset r, where r ∈ 2C , we shall intorcuce a function denotedby r(v), and let r(v) = v[x *→ 0], x ∈ r. For each location
invariant I, we shall introduce a function denoted by I(l)(v),
which stands for the valuation of the location invariant I(l) of
location l with the clock valuation v.
Dynamics of a timed automaton can be expressed via a setof states and their evaluations. Changes of one state to a newstate can be as a result of firing of an action or elapse of time.

The term “line trace” means that a vehicle traces a course
starting from a certain point. The point might be on the course
or not. The course is assumed to be painted in black color on
white background with the same width. For example, an oval
course (the same as the track used in an athletic field) is used.
A model for a line tracer consists of the following threemodels:• Controller Behavior,• State Transition of Environment, and• Disturbance.
Controller behavior can be modeled using a state machine.
Usually, controller program changes values of some of statevariables based on values of some state variables.
For example, the state variables of a line tracer will be thelocation of the tracer, the locations of the right and left sensors, the output values of the right and left sensors, directionof the line tracer, the rotation speed of left and right wheels,and so on.
The output values of the right and left sensors are used as
inputs of the controller. The rotation speed of left and rightwheels are used as outputs of the controller

Definition 3 (state of timed automaton) For a given timed
automaton A = (A, L, l 0 , C, T, I), let S = L × RC
≥0 be aset of whole states of A , where RC≥0 is a whole set of clock
evaluation on C.
The initial state of A can be given as (l 0 , 0C ) ∈ S.
a,g,r
For a transition l1 → l2 , the following two transitions aresemantically defined. The first one is called an action transition, while the latter one is called a delay transition.

137

variable
x:
y:
θ:
slx:
sly:
srx:
sry:
wl:
wr:
sl:
sr:

Table 1: State Variables of a Line Tracer
description
x-coordinate of the center of a line tracer
y-coordinate of the center of a line tracer
direction of a line tracer
x-coordinate of the left sensor of a line tracer
y-coordinate of the left sensor of a line tracer
x-coordinate of the right sensor of a line tracer
y-coordinate of the right sensor of a line tracer
revolution speed of the left wheel of a line tracer
revolution speed of the right wheel of a line tracer
the sensed value of left sensor
the sensed value of right sensor

Table 3: Conversion Table for Sine Function
domain of x (degree) round of 100× sin(x)[0, 10)8[10, 20)
26[20, 30)42[30, 40)
57[40, 50)
71[50, 60)
82[60, 70)
91[70, 80)
96
..
..
.
.
[350, 360)-9w hs + l s
·
rc =
(4)
Table 2: Constants
2 hs − l sconstant descriptionw:width between left and right wheels of the line tracer
Disturbance can be modeled as uncertain error for each oflos:offset to the left sensor from the vehicle center
observation variables. For example, a line tracer has sensors.
ros:
offset to the right sensor from the vehicle center
The value s, the output of the sensor may change with uncerlos, ros are tupple of (l, a), where l and a are the distacbe
tain value as like the following equation:
and angle by the center of the vehicle, respectively.
so = sr + ε(s), where variables s o , sr , and ε(s) represent theobserved value, ideal value and error in observation, respectively.

State transition of environment can be normally represented
in differential equations on state variables. In a hybrid system, such equations are used, while in a finite sate model,
differential-difference equations are used as approximation.
For a line tracer, the principle state variables are summarized in Table 1.
We need some other constants to model, especially constants on the size of the line tracer. Table 2 shows some ofthem. Figure 1 also illustrates the relations on the state variables and constants.
Let assume that a line tracer turns with the speed of left andright wheels at hs and ls . Then equations of motion can begiven as follows.
dθ
dt
dx
dt
dy
dt

=

hs − l sw=−rc · sin θ ·=3.1 Quantization(2)

The timed automaton used in UPPAAL can model the controller behavior. It, however, uses integer variables only. As
we know, most of state variables must have values in real.
Therefore, we have to approximate such variables into integer variables.
Most of state variables use trigonometric functions (seeequations (2) and (3)). Thus, we have to approximate thefunctions to round up into integers as long as we use finite
models. Though, the values of trigonometric functions range
in [-1,1], it is not a good idea that we use only three values-1, 0, and 1. Therefore, we assume that trigonometric functions range in [-100, 100]. Also we adopt degree as unit forangle. Table 3 shows an approximation conversion table forsine function.

(3)

3.2 Sampling

(1)

dθ
dt
dθ
rc · cos θ ·dt

Yet another problem is that we cannot deal with functions
on time. Usually state variables can be represented as function on time, however, even UPPAAL does not provide functions on time. Therefore, we have to regard state variables as
discrete signals.
Sampling is a great tool to reduce a continuous signal into a
discrete signal. For a discrete signal, we can model its change
on time as an timed automaton with update functions.
Let’s consider again state variables, x, y, θ, slx, sly, srx,
sry, wl, wr, sl, and sr. In usual, slx and sly are calculatedusing x and y with some parameters in Table 2. The valuesof sl and sr are also determined from the value of x, y, los,ros, and a course model, which consists of some parameters
and the equations of the course. The values of wl and wr are
determined by the controller.

!')", ')$%+(, +)!'(", '($%
)*'
&
(*'
!", $%+

Figure 1: Constants and State Variables

138

import lejos.nxt.Button;
import lejos.nxt.ColorSensor;
import lejos.nxt.SensorPort;
import lejos.nxt.ColorSensor.Color;
import lejos.nxt.LCD;
import lejos.nxt.Motor;
public class Controller {public static void main(String[] args)
throws Exception {int rid,lid;
final int HS = 420, LS = 120, BLACK = 7,
MS = 360, HSEC = 500;
Color colorR ,colorL;
ColorSensor sensorR =new ColorSensor(SensorPort.S3);// 1(S3):right
ColorSensor sensorL =new ColorSensor(SensorPort.S4);// 2(S4):left
Motor motor = new Motor();motor.B.setSpeed(MS);motor.C.setSpeed(MS);Thread.sleep(HSEC);// wait for devices to be stable
motor.B.forward();motor.C.forward();while(true) {rid = sensorR.getColorID();lid = sensorL.getColorID();if (rid == BLACK)
motor.B.setSpeed(LS);elsemotor.B.setSpeed(HS);if (lid == BLACK)
motor.C.setSpeed(LS);elsemotor.C.setSpeed(HS);if (Button.readButtons()== Button.ENTER.getId())
break;}}}

Table 4: Logic for Color Sensors
RightSensor
black
white
LeftSensor black go straightturn left
white
turn right go straight
Therefore, we need calculate the current value of x, y andθ like as equations (1) ∼ (4).
Using sampling and update functins, we can model that thevalues of variables are updated every some fixed unit of timeusing small deltas. We will explain concrete update expressions in Sec. 5.

4IMPLEMENTATIONLEGO Mindstorms NXT[9] is a kit for assembling robots
Rwith various actuators and sensors by LEGO #. Users canprogram its behavior. The actuators include stepping motors
which users can accurately control rotation angles. The sensors include color sensors, touch sensors, sound sensors andso on. Various programming languages are provided for control of the NXT kit. The famous languages are NXC (NoteXactly C)[10] and LeJOS. LeJOS is a development environment for Java. NXC and LeJOS have classes for the above
sensors and actuators.
This research uses LeJOS for developing the line tracer.
Our line tracer has two color sensors locating left front andright front of the tracing car.
Table 4 shows the logic for the sensors. For example, if
LeftSensor and RightSensor sense white and black colors, respectively, then the controller issues the turn right command
to motors.
The output of sensors is a bounded integer value. If thevalue is greater than some threshold, then controller treats it
as white. For the command, left and right wheel motors react
independently. For example, “turn left” command makes left
and right wheel motors speed up and dowm, respectively
Figure 2 shows the controller in LeJOS. Figure 3 shows theimplemented line tracer.

5

EXPERIMENTS

Figure 2: Controller in LeJOS

Here, we deal with an ideal model. Therefore, we ignore
disturbance. Figures 4 and 5 corresponds to controller behavior model and state transition of enviroment model. In
this experiment, we use a simple controller program, where
revolution speed of wheels has only two values, h s and ls .
Moreover we assume that sensors only tell white and blackcolors on the track. In other words, the values of sl and sr
are determined by only the position of the line tracer. On
the other hand, we model the delay of sensors and actuators.
Concretely, we have parameters d s , da , and dt for delay between the time when program senses color and the time when
the sensors obtain the values of colors, delay between the time
when program issues a command and the time when the motor
reacts, and sleeping time for next sense-act loop, respectively.
This modeling represents real behavior of a line tracer.
Figure 4 shows the control behavior model of the program.

Figure 3: The Implemented Line Tracer

139lsensorL==black &&lsensorR==white &&t == sdt <= cdturnLeftstart
t <= sdt == cd
lws=ls,rws=hs,dir=LEFT,t:=0t := 0t <= cd
turnRight

lsensorL==white &&lsensorR==black &&t == sdt := 0t <= cd
unwantedlsensorL==black &&lsensorR==black &&t == sdt := 0lsensorL==white &&lsensorR==white &&t == sdt <= cd
goStraightt == cd
lws=hs,rws=ls,dir=RIGHT,
t:=0paramswc:
w:

sleepStatet <= sleep

los:

t==cd
lws=hs,rws=hs,dir=STRAIGHT,
t :=0

ros:

t == cd
lws=hs,rws=hs,dir=STRAIGHT,t:=0t := 0t == sleep

hs :
ls :
x0 :

t := 0,lsensorL = lsensor,
lsensorR = rsensor

Figure 4: Timed Automaton Representing the Controllert <= 1

y0 :
θ0 :
ds :
da :
ds :

t == Pt := 0lsensor = updateL(theta, dangle),rsensor = updateR(theta, dangle)

x = updateX(x,theta,hs,ls,dir,S,L),y = updateY(y,theta,hs,ls,dir)theta = updateT(theta,da,dir)Table 5: Parameters under Verification
value description
100 width of the track line
120 width between left and right wheels of
the line tracer(180, 30◦ ) offset to the left sensor fromthe vehicle center(180, −30◦) offset to the right sensor fromthe vehicle center
12 high speed
6 low speed-200 initial value of x-coordinate of the centerof the vehicle
200 initial value of y-coordinate of the centerof the vehicle340◦ initial value of direction of the vehicle
1 time delay of sensors
1 time delay of actuators
2 periodical sleeping time

5. A"¬(C.unwanted).
6. E♦(C.goStraight).

Figure 5: Timed Automaton Representing Update

7. A"((x > 280) ⇒ (−100 < y < 100)).
8. A"((x > 280) ⇒ (θ < 10 ∨ 350 < θ)).

Figure 5 shows the timed automaton which updates periodically state variables every unit of time. The automaton periodically calls functions updateX, updateY, updateT, updateL, and updateR which update state variables x, y, θ, sl,and sr, respectively. The automaton first updates the value ofθ, and then values of x and y. Finally it updates values of sland sr based on the values of x, y, and θ.
The following equations are equations for θ, x, and y usedin update functions.
θ"

=

"

x

=

y"

=

α =

θ+α
wl + wrcos θx+2
wl + wrsin θ
y+2
wr − wl
90 ·w·π

9. E♦((x > 280) ⇒ C.turnRight).
10. E♦((x > 280) ⇒ C.turnLeft).
The first query (1) means that the line tracer will reach thearea x > 900. Queries (2) and (3) mean that the controller
eventually reach state C.turnRight and C.turnLefit. Queries(4) and (5) mean that the controller eventually reach state
C.unwanted and that the controller never reach state C.unwanted,
respectively, where both of sensors detect black color. Query(6) means that the controller eventually reach state C.goStraight.
Queries (7), (8), (9) and (10) uses the assumption that aline tracer is in stable state. Please note that we think after the
point x = 280, the tracer is in stable. We can observe it fromseveral traces of simulation. The traces can be obtained fromthe UPPAAL using the simulation mode view.
Queries (7) and (8) mean that the line tracer roughly keeps
the track and appropriate direction, respectively, in the stablestate.
The last two queries mean that the line tracer eventuallyturns left or right even if the tracer is in stable state.
Every of the verifications (except the query (4)) has succeeded with the parameters in Table 5. Every verification is
performed within one sec. using UPPAAL ver. 4.0.13 academic licence on Windows 7 64 bit OS, Intel Core i7 960
3.20GHz, with 12 GB memory.
Query (4) passed if we change the parameter los and ros
as (170, 30◦ ) and (170, -30 ◦ ). In this time, of course, Query(5) changes to false.
We assume that if the value of x becomes greater than 1000
then the value of x is reset to 50. This device let a line tracer
run infinitely in the finite state model.
Figure 6 shows verification process using UPPAAL.

(5)
(6)
(7)
(8)

If we assume that the unit of time is small then the moving
distance of the vehicle can be approximated to (h s + ls )/2.
The above equations uses this fact.
Please note that we actually use not sin but pseudo sin /100
defined in Table 3. Also we let the values of the parameter p
range in [0, 360] by using an expression (p + 360)%360.
We also assume that the course is a straight line along with
x-axis.
We can verify the following queries:
1. E♦(900 < x).
2. E♦(C.turnRight).
3. E♦(C.turnLeft).
4. E♦(C.unwanted).

140

cannot response in a reasonable time or exhausts whole ofthe memory space.
Nevertheless such situations, it shows the importance ofdesign analysis and verification in an early stage of development.
During the modeling, we think that there should be an automated generation tool which translates from an abstract parameter model to a concrete UPPAAL model, as well as asimple tool to analysis counter-examples and simulation results obtained from UPPAAL. They would be very useful torefine the model.

6.2 Hybrid System
In order to analyze the model more precisely, hybrid systems seem promise models.
Hybrid system[11] is a system in which continuous dynamics and discrete dynamics are mixed with time progress. Hybrid systems are important in many fields such as physics andcontrol engineering. Several approaches are proposed to deal
with hybrid systems. One of the approaches is hybrid automaton[12] which is a formal model for describing mixed
discrete-continuous systems. Hybrid automaton consists ofvariables, control graph, continuous flow, discrete jump andevents. A model checker for linear hybrid automata is HyTech[13].
Another approach is hybrid constraint languages such as Hybrid cc[14] and HydLa[15]. These languages are declarativeand provide power to write programs with logical formulas.
Execution environment of these languages are implemented,
Hybrid cc interpreter and Hyrose, respectively.
A line tracer can be a hybrid system by describing its movement using differential equations and its control program indiscrete time. However, there are difficulties if a line tracer ismodeled accurately. For example, modeling with characteristics of motors and sensors, and disturbances are difficulties.
Fehnker et al. presented a study of verification of behaviors
of a line tracer[16]. In the paper, the authors presented verification of a safety property, a line tracer move along a straightline and never run off the line, by constructing a model using
hybrid I/O automata and correctness proof. However, as theauthors mentioned, some kinds of time is not considered suchas time delay between two motors.

Figure 6: Verification using UPPAAL6DISCUSSIONS

Here, we will describe discussions on the experiments andhybrid systems.

6.1 Discussions on The Experiments
The results are not enough to convince us that the line tracer
runs safely. The results, however, show that from the theoretical point of view, our approach using a verifier for timed
automata, will work.
The parameters used in verification are not the same to theparameters used in the implementation. This might lessen thevalidity of the model. However, the proportional relations of
the parameters are acceptable. For example, the width ws
between the left sensor and the right sensor is 190 and it isgreater than 100, the width of the track.
The value ws is greater than 120, the width of the line
tracer. It is very different from the implementation in Figure
3. The parameters are, however, acceptable. Also the wheel
speed 6 or 12 is acceptable with regard to the size of the line
tracer.
The workload of modeling is in fact not less (it takes over
2 month-persons) due to our limit of know-how on modeling,
especially how to deal with continuous model. Some of parameters in Table 5 are very sensitive, in other words, if thesevalues are different by a little, the behavior of the whole system differs; consequently, verification will fail. For example,
with the parameters in Table 5 if we change the value of d s as
4, then the verification fails.
You might think that slow wheel speed increases the possibility of success of verification. In other words, the slower
a line tracer moves, the more successively it keeps the track.
However, due to the quantization, a small wheel speed causes
the delta values per unit of time to be 0 in our model. Therefore, we cannot set smaller value than 6 as the low speed of
the wheel. Such a problem can be resolved by increasing thephysical sizes in the model. However, such a revise, in turn,causes so called state explosion in which a model checker

7 CONCLUSION
We have modeled a controller of a line tracer in timed automata. Also we have verified the model to ensure that theline tracer keeps the track, using a model checker, UPPAAL.
Future plans are summarized as follows. First, we want tomodel a PID controller (proportional-integral-derivative controller), which is a kind of feedback controls. PID control
enables a line tracer to behave more smoothly. PID control,
however, needs some historical data on the past values of statevariables, and also requires complicate calculation, thus hybrid modeling becomes more suitable. We want to use hybrid
model, as well as its verifiers and simulators to determine suitable parameters for PID control. It is said that to find suitableparameters for PID control for an instance of problems, is141

In Lecture Notes in Computer Science, vol.999, pp.226251 (1995).
[15] K. Ueda, H. Hosobe, and D. Ishii: “Declarative semantics of the hybrid constraint language HydLa,” Computer Software, JSSST, 28(1) pp.306-311 (2011). (inJapanese).
[16] A. Fehnker, F. W. Vaandrager, and M. Zhang: “Modeling and verifying a lego car using hybrid I/O automata,”
In Proc. of 3rd Int. Conf. on Quality Software, pp.280289. IEEE Computer Society (2003).

a difficult problem for a long time. We think our approach
might work well.
Another direction of our research is timing analysis of motor delay. From preliminary experiments, we have found thatmotor delay cannot be ignored for design of controller program if we want to obtain a high quality controller.

ACKNOWLEDGEMENT
This research is partially supported by Grant-in-Aid for
Scientific Research (C) (21500036).

REFERENCES[1] R. Alur and D. L. Dill: “A theory of timed automata,” Journal of Theoretical Computer Science,
126(2), pp.183-235 (1994).
[2] J. Bengtsson and W. Yi: “Timed Automata: Semantics,
Algorithms and Tools,” In Lecture Note in Computer
Science, vol.3098, pp.87-124 (2004).
[3] J. Bengtsson, W. O. D. Griffioen, K. J. Kristoffersen, K.
G. Larsen, F. Larsson, P. Pettersson and W. Yi: “Verification of an Audio Protocol with bus collision using UPPAAL,” In Lecture Note in Computer Science, vol.1102,
pp.244-256 (1996).
[4] M. Lindahl, P. Pettersson, and W. Yi: “Formal Design
and Analysis of a Gear Controller: An Industrial Case
Study using UPPAAL,” In Lecture Note in Computer
Science, vol.1384, pp.289-297 (1998).
[5] B. Bordbar and K. Okano: “Verification of Timeliness QoS Properties in Multimedia Systems,” In Lecture Note in Computer Science, vol.2885, pp.523-540(2003).
[6] J. Fitzgerald, P.G. Larsen, K. Pierce, M. Verhoel, and S.
Wolff: “Collaborative Modelling and Co-simulation in
the Development of Dependable Embedded Systems,”
in Proceedings of IFM 2010, pp.12-26 (2010).
[7] B. Bagnall: “Intelligence Unleashed: Creating LEGONXT Robots with Java,” Variant Press (2011).
[8] LeJOS Java forLEGO Mindstorms:
http://lejos.sourceforge.net[9] LEGO Mindstorms NXT Official website:
http://www.legoeducation.jp/mindstorms/[10] NXC Tutorial:
http://bricxcc.sourceforge.net/nbc/
nxcdoc/NXC tutorial.pdf[11] J. Lunze and F. Lamnabhi-Lagarrigue: “Handbook ofHybrid Systems Control: Theory, Tools, Applications,”
Cambridge University Press (2009).
[12] T. A. Henzinger: “The theory of hybrid automata,” In
Proc. of Eleventh Annual IEEE Symposium on Logic in
Computer Science, LICS ’96, pp.278-292 (1996).
[13] T. A. Henzinger, Pei-Hsin Ho, and H. Wong-Toi:“HYTECH: A model checker for hybrid systems,” In
Lecture Notes in Computer Science, vol.1254, pp.460463 (1997).
[14] V. Gupta, R. Jagadeesan, V. Saraswat, and D. G. Bobrow: “Programming in hybrid constraint languages,”142