Stepwise Approach to Design of Real-Time Systems based UML/OCL
with Formal Verification
Takeshi NAGAOKA† , Eigo NAGAI† , Kozo OKANO† , and Shinji KUSUMOTO††

Graduate School of Information Science and Technology, Osaka University
Machikane-yama 1–3, Toyonaka City, Osaka, 560–8531 Japan

Abstract - This paper provides a stepwise method for thedesign of real-time systems with timeliness QoS guarantees.
In the proposed method, the system components are designed
using UML diagrams and are provided with the timelinessQoS annotated with OCL. The basis of this technique is to formally ensure that the required timeliness QoS is satisfied under the provided timeliness QoS, given the network property
and the UML diagrams. In order to avoid the state-explosion
problem during performance model checking, which can logically check the satisfiability, the problem is separated into two
steps. The first step checks the satisfiability using an abstract
model of each of the components derived automatically fromthe provided QoS. The second step independently performs
model checking for each of the components using a more detailed version of the behavioral model of a given component.
Such an approach reduces the number of total states to check.
Furthermore, the approach can be extended into hierarchicaldesign, which leads to good scalability. Experimental results
are also included in this paper.
Keywords: timeliness QoS, UML/OCL, model checking,component based systems, hierarchical design

1 Introduction
This paper presents a new method to verify consistency oftimeliness QoS of component-based designed real-time systems. We assume that timeliness QoS is not only given to awhole system (Required QoS) but also associated with eachcomponent of a given system (Provided QoS).
Timeliness QoS is a time aspect of QoS (Quality of Service) features[1]. In the paper, we treat jitter, latency andthroughput as timeliness QoS.
Nowadays, most real-time systems are designed with helpof UML diagrams[7]. Especially components and their relation through signal communication can be represented ina class diagram of UML. In UML based design, such timeliness QoS can be annotated in OCL[8]. The annotation isassociated to each of components as a provided QoS and also
to a network link as a network property. Recently, SysML(System Model Language)[13] also attracts interest. SysML
extends from UML and presents mixed systems consisting ofphysical devices and software and network systems. Therefore, SysML supports diagrams for signal flows and physicalflows. For behavioral diagrams, SysML supports four diagrams as same as UML. Among them, state diagram has powerful representation including parallel and hierarchical states.

The proposed method is revised version of paper [15]. The
method in [15] uses Linear Programming (LP) for some ofverification. The approach has a disadvantage that connection among components has to be acyclic, and it cannot beapplied to hierarchical design. The method of this paper uses
abstract QoS automata instead of using LP; thus it improves
the former disadvantage.
The heart of the technique is formally to ensure that therequired timeliness QoS is satisfied under the provided timeliness QoS, given network property and the class diagram.
In order to check the satisfiability, there are several approaches. Formal approaches are very useful. Model checking is one of such an approaches. Notion of Test Automata[3],[5] and its application is also useful. However, one of disadvantage of the method is the state-explosion problem.
In order to avoid state-explosion problem while performing model checking, we separate the problem into two steps.
The first step checks the satisfiability using abstract model ofeach of components derived automatically from the provided
QoS. The second step performs model checking each of components independently using more detailed version of behavioral model of a component. Such an approach efficiently
reduces the number of total states to check. Moreover the approach can be extended into hierarchical design; therefore it
has good scalability.
SaveCCM[14] is a technique for Component based Development (CBD). In a description of a component, it allows user
to define ports where signals input or output and to represent
behavior in a timed automaton[2]. An IDE over Eclipse isavailable. Therefore, our proposed method has an affinity for
SaveCCM.
The paper organized as follow. Section 2 gives timeliness
QoS. Section 3 shows how to design component based realtimed systems in UML/OCL. Section 4 demonstrates the proposed method which consists of two steps. Section 5 provides
an experimental example. We conclude the paper in Section
6.

2 Timeliness QoS
Main building blocks of our model are components. Eachcomponent has one or more interfaces to the environment,
where all interactions between components is conducted via
the interfaces. Since, we are mostly dealing with real-timesystems and timeliness QoS, we shall assume that the interaction of a component with its environment is carried out via

<< component >>A<< component >>data_flow((a1,b1),(a2,b2))<<QoS>>throughput(a1,100)<<QoS>>throughput(a2,100)

B<<QoS>>jitter(b1,5)<<QoS>>delay(b2,b3)<< network >>A_B

Throughput Variable := “throughput(” signal “,” period“)” ;Jitter Variable := “jitter(” signal “,” period “)” ;Latency Variable := “delay(” output “,” input “)” ;<<QoS>>network_delay

Figure 1: A Configuration of Components in UML Class Diagram
input and output signals. As a result, interfaces of a component specify signals that the component receives or emits.
Each component is associated with a number of input andoutput signals. In this paper, signals are denoted by x, y and z.
Time of occurrence of a signal is denoted via a non-negative
sequence of rational numbers. For example, the time of occurrence of a signal x is denoted with x1 , x2 , . . . representing
time of first, second, ... occurrence of x.
Timeliness QoS expressions [9] such as jitter, throughput
and latency can be expressed via first-order logic formulas on
the set of time of occurrence of signals.
Throughput of at least (most) K within the time period T,
for signal x can be written as the first order formula ∀i ∈N : xi+K−1 − xi ≤ T (∀i ∈ N : xi+K−1 − xi ≥ T ),respectively.
Notice, paper [5] refers to the above QoS constraint as NonAnchored throughput.
Jitter , also called Non-Anchored jitter , of a signal x can be
defined by the expression ∀i ∈ N : T − m ≤ xi+1 − xi ≤T + M, where T is the period of the jitter and m, M are
constant rational numbers.
Latency of at most T unit of time between two signals x andy as ∀i ∈ N : 0 < xi − yKi+K ′ ≤ T. A special case of theabove definition (for K = 1 and K ′ = 0) is the well-known
definition of latency ∀i ∈ N : 0 < xi − yi ≤ T that applies
to the time difference of the i-th occurrence of x and y.

A class with “component” stereotype has three categories
of timeliness QoS (Jitter, throughput and latency), while aclass with “network” has two categories of timeliness QoS(Jitter and latency).
The OCL description is given as follows[9].
QoS description := “context” className invariant* ;invariant := “inv: self.” constraint ;constraint := variable op constant;variable := Throughput Variable | Jitter Variable | Latency
Variable
op := “>” | “<” | “≥” | “≤” ;For example, the following are examples for Fig. 1, where– means a comment line.
context A
inv: self.throughput(a1,100) ≥ 20
– signal a1 is emitted at least 20 times in the period 100
units of time
inv: self.throughput(a2,100) ≤ 10
– signal a2 is emitted at most 10 times in the period 100
units of time
context B
inv: self.jitter(b1, 5) < 1– signal b1 has jitter 1 with period 5 units of time
inv: self.delay(b2,b3) < 5– latency between receiving signal b2 and sending signal b3 is less than 5 units of times
context A B
inv: delay ≤ 100– latency (network delay) between component A andcomponent B is less than 100 units of time

4 The Verification Method
3 UML/OCL based design of real-timesystems
A real-time system can be designed as a set of components
where signal communication links exist among pairs of components. We can describe such components in a UML class
diagram in Fig. 1.
Type Component can be specified by Stereotyping “component,” by which user can easily extend UML specification.
A signal communication can be specified with Association.
Each of components has provided QoS, which can be represented via OCL annotation. Each of network links (which
has association class with stereotype “network” ) also has network properties represented via OCL annotation. The network properties is the same as timeliness QoS. Attribute region of each class, includes special variables for QoS with
“QoS” stereotype (in Fig. 1).
The following is the syntax of the variables.

The verification consists of two steps; First Step and Second Step.
If some of the components are not simple enough, then repeat the process again from First Step on each of the components.
The following is the abstract level of steps of the proposed
method.
input:• system required timeliness QoS represented in OCL;
• component level provided timeliness QoS represented
in OCL; and• network configuration represented in UML/OCL class
diagram.
output:• component level behavioral specification represented in
UML/OCL state-chart which satisfies required timeliness QoS under the configuration;

x!
x!

c<M

t:=0, c:=0

c++
T>=t

• or failure.
c==M

1. First step(a) We generate test automaton form the required timeliness QoS.

x!
t :=0, c :=0

Figure 2: Abstract QoS automaton for Anchored Throughput(b) We generate abstract QoS automaton form eachof the provided timeliness QoS.
t >= T- d0(c) We generate configuration automaton form the network configuration.

x!
t:=0

(d) We check the consistency from parallel composition of the above automata.
(e) If the result is deadlock then return failure. We
have to reconfigure the requirement or provided
conditions.
(f) If the result is not deadlock then go to Second
Step.
2. Second Step(a) If the component is not small enough to represent
simple state-chart, then refine the component by;i. renaming provided QoS of the component torequired QoS;
ii. design sub components and provided QoS ofeach of them;iii. design network configuration; andiv. we repeat the First Step until the component
is enough to small.
(b) If the component is small enough to represent simple state-chart, then we describe state chart of thecomponent.
(c) We translate a test automaton from the provided
timeliness QoS.
(d) We design network of timed automata from thestate-chart.
(e) We check the consistency from parallel composition of the above automata.

t <= T+d1

Figure 3: Abstract QoS automaton for Non-Anchored Jitter
The output is whether a given required QoS is satisfied under a given set of components with provided QoS and a given
set of network links with network properties.
In usual methods, designer models behavior of each component in a network of timed automata and for the whole network of timed automata. Then the designer performs model
checking, which often results in state explosion.
Here, we give a new method, in which timed automata (Wecall each of them an abstract QoS automaton) is derived
automatically from the provided QoS.
The important point is that derived automata are so smallthat state-explosion is avoided.
Here, we give a translate rule for each provided QoS.
4.1.1 Throughput
For a component with anchored throughput with parameter
max:M , min:m and period:T , we give an abstract QoS automaton in Fig. 2.
4.1.2 Jitter
For a component with non-anchored jitter with parameter max:M ,min:m, we give an abstract QoS automaton in Fig. 3.

(f) If the result is deadlock then return failure. We
have to reconfigure state-chart.

4.1.3 Latency(g) If the result is not deadlock then return success.

For a component with latency with parameter max:M , min:m,
we give an abstract QoS automaton in Fig. 4.

4.1 The First Step
Verification inputs are the following.
• Required QoS;
• a set of components with provided QoS; and• a configuration automaton which represents network properties.

y?
t:=0
t<=M
t>=m
x!
t:=0

Figure 4: Abstract QoS automaton for Latency

t >= T0 && t <= T &&c == it := 0,e?
c := c + K
sleep

c == iactivet0 <= Tt0 >= T - delta0, t0 < Te?

failuree?
t := 0,c := c + K

t0 < T - delta0
e?

failuree?

Figure 5: Test Automaton for throughput

t1 <= T + delta1
e?

t1 == Tt0 := 0s2

t1 >T + delta1
e?

sl21

se21
t1 <= T

t1 == Tt0 := 0t1 >= T - delta0, t1 < Te?

Figure 6: Test Automaton for jitter

4.1.4 Configuration Automaton
A configuration automaton models interfaces among components. As each component has several inputs and outputs,
such an I/O is represented as a channel in the configuration
automaton. Each channel synchronizes with some I/O of somecomponents with provided QoS (abstract QoS automaton).
Abstract QoS automata and the configuration automaton communicate each other as described above.

t1 < T - delta1
e?

t1 <= Tt0 <= T

Unfortunately, the automaton does not accept input y until
it emits output x. To avoid the problem, a set of the same
automata is needed. The number of automaton decided fromthroughput property of the components.

e?

s1
e?
t0 := 0, t1 := 0

t0 == Tt1 := 0t0 <= T + delta1
e?

t0 > T + delta1
e?
s0

t < T0 && c == i
e?

sl12

t0 == Tt1 := 0t>Tse12cx == ix?
t := 0, cx := cx + K
cy == i && t > Ts1s0cy == i && t <= Ty?
cy := cy + K

y?
failureFigure 7: Test Automaton for latency

4.1.5 Test Automaton
Here, we give each test automaton for throughput, jitter andlatency[10].

For the detail of process of the verification, refer [10].
4.1.7 Category Based Model Checking

Throughput For a non-anchored throughput of which a signal e occurs at least k times in a period T , a network of test
automata consisting of k processes of timed automata in Fig.5
observes the throughput. In the network of test timed automata, the variables c is shared among automata globally.
Each of timed automata is activated by turns along the valueof variable K.

Verification is performed for every timeliness QoS category(latency jitter and throughput). The idea and approach is very
simple. When we want to check only latency as the required
QoS, we build an abstract automaton for provided QoS of latency only.
The divided and conquer approach, reduces the size of states.

Jitter Figure 6 shows a test automaton for anchored jitter. It
observes whether a signal e occurs periodically in the period[nT − delta0 , nT + delta1 ], where n = 1, 2, 3, . . ..

For each of components, Second step has the following twocases depending on the component’s abstraction

Latency Figure 7 provides a component of test automata
for latency between a signal x and y.
T/D processes of component in Fig. 7 observes latency atmost D unit of times of the latency.

• We design detail behavior of the component and verify
whether provided QoS is ensured by the design.

4.1.6 Verification
The behavior of such media with timeliness property also ismodeled in a network of timed automata, we call such an automaton a configuration automaton.
Parallel composition of an abstract automaton for every
component and the configuration automaton and test automaton for specified timeliness QoS decides whether the wholesystem satisfies the specified timeliness QoS.

4.2 The Second Step

• We repeat First step to the given component recursively.

If the size of the given component is large and designer has
to design the given component from more detail components,
then repeats First step.
Hereafter, we describe the later case.
At Second step (of the later case), verification is independently performed for each component.
Before Second step, the designer has to give detailed behavior of each component. Such behavior is given in UML
state-chart. In order to give time constraints on events, thestate-chart has clocks.
Verification inputs are the following.

UML
Statechart

Timed
Automata

Test Timed
Automata

MS_Storage
OCL

MS_Controller

Digital_TV

y1!

UPPAALx3?

x2?

Figure 8: Verification on UPPAAL based on Test Automata

x1?
y3!
c_DTFrame < MAX_FRAME
c_DTFrame++,c_AudioFrame := 0
Audio_System• component’s behavior given in UML state-chart withclocks; and• component’s provided QoS.
The output is whether provided QoS is satisfied under agiven UML state-chart with clocks.
The verification is performed based on test automaton. We
have to translate a UML state-chart with clocks to a networkof timed automata.
A state-chart can represent hierarchical architectures; whilea network of timed automata is a simple flat structure model.
In general, hierarchical structure can be flatten, but such translation increases the number of states. There are several translations, and this paper adapts the one in [4]. The translation itself is an algorithm to translate Hierarchical Timed Automata(HTA) to a network of timed automata used by UPPAAL[11].
Thus, we have to translate state-charts to HTA. Fortunately,
syntax and semantics of state-chart and HTA are both similar,
the translation is simple.
We add the following constraints on the state-chart.
• the state-char diagram has clocks; and• arcs in the stat-chart has clock constraints in a form of
the one same as Timed automata in UPPAAL.
We also use test automata to check timeliness QoS. Test
automata for jitter, latency and throughput are given in 4.1.5.
The verification can be performed with UPPAAL. Thanks
to test automata, we just check deadlock property for each
QoS. Logical expression for deadlock property in UPPAAL
is “A[] not deadlock.”

5 Experiment
The proposed method is applied to an example.

5.1 The example
Media Server is an application delivering video stream andaudio stream to Digital Television and Audio System[6], [12].
Each of output devices required timeliness QoS (throughput).
Figure 9 shows the class diagram of the application, which
consists of twelve components.
In order to compare the proposed method to the old method,which uses LP solver to First Step, we merge the twelve components to three components (Server 3 components , Audio
client 4 components, and Video clients 5 components).

x4?
y2!
MS_Server c_AudioFrame < MAX_FRAME
c_AudioFrame++, c_DTFrame := 0

Figure 10: The configuration automaton

5.2 First Step
The following is the provided QoS.
• Throughput of Component MS–Server is equal or greaterthan 100 frames/s.
• Processing latency of Component MS-Storage is equal
or less than 5ms.
• Network latency between MS–Server and Digital–TV
is equal or less than 100ms.
• Network latency between MS–Server and Audio–System
is equal or less than 150ms.
For these provided QoS, and a configuration automaton derived from the UML class diagram, and Required QoS for thewhole system, we apply the verification along with First Step.
Here, we performed verification under the condition thatthe throughput of Digital Display (DT Display) is over 30
frames/sec as Required QoS.
Figure 10 shows the Configuration automaton for the experiment. The Configuration automaton in Fig.10 represents
connection among the components. It uses channels to communicate abstract QoS automata providing the provided QoS
mentioned above. For example channel x is used for communication to an abstract QoS automaton with throughput 100
frames/sec at a transition between MS–Controller and MS–
Server. In order to avoid unfairness that frame communication occurs only between MS–Server and Digital–TV (or only
between MS–Server and Audio–System), we use a parameter M AX F RAM E, which is used in a condition that the
maximum successive occurrence of signals between the same
components. We use a condition M AX F RAM E = 1 forthe experiment.
Figure 11 shows the test automaton for throughput as Required QoS. The test automaton observes throughput of 3frames per 100ms. As required QoS, the required value ofthroughput is 30 frame/sec, We have to need 30 processes ofthroughput test automata to observe the throughput exactly.
At the First Step, we have performed verification experiments for two configurations: (1) an abstract QoS which outputs ten frames per 100 msec, and (2) an abstract QoS which

Digital-TV

Media Server
MS-Storage

MS-DT_network

DT-Receiver

MS-Controller

DT-Controller

DT-L-Speaker

DT-display

DT-R-Speaker

Audio-System

MS-Server

AS-Receiver

AS-Controller

MS-AS_network

AS-L-Speaker

AS-R-Speaker

Figure 9: Class Diagram of Media Server# of P
3
6
9
12
15
30

Table 2: The result (2) of first step
result
CPU time Used memories
not valid
0.6 ms
23.9MBnot valid
0.7 ms
24.4MBnot valid
1.2 ms
24.7MBnot valid
1.6 ms
25.0MBnot valid
2.1 ms
25.1MBvalid
957 ms
40.4MBon

Figure 11: The network of test automata for the given required QoS

off

off

# of P
3
6
9
12
15
30

Table 1: The result (1) of first step
result
CPU time Used memories
not valid
0.3 ms
23.9MBnot valid
1.4 ms
24.4MBvalid
28 ms
24.8MB
valid
50.6 ms
25.9MBvalid
83.6 ms
26.8MBvalid
480 ms
34.4MB

outputs 30 frames per 300 msec, respectively, are used for abstraction of provided QoS for MS.Server. Each of two experiments is performed with several numbers of test automata: 3,6, 9, 12, 15 and 30. We have obtained CPU times and sizesof memory consumed. The experiments are performed in thefollowing environment: CPU is Intel Core 2 Duo 2.33GHz,
OS is Windows Vista Business and M.M. is 2GB. We used
UPPAAL4.1.0 as a model checker. Table 1 and Table 2 show
the results of (1) and (2), respectively. The column of “# of P”
shows the number of processes (the number of test automata).

on

/T:=0

search MS-in[T>2]/MS-out,T:=0

T<=2

control

pack

error

/errorFigure 12: A UML Statechart Diagram of Component MSStorage
In the previous experiment, we have performed First Step
with Linear Programming solver. In the experiment, we have
performed it in 78 ms (although it has been performed in different environment).

5.3 The Second Step
After First Step, we design inner behavior of each component.
In the example, recursive application of First Step is not
performed, because each component is small enough. Behavioral specification is described in UML state-chart. The
design must meet the provided QoS. Figure 12 shows behavioral specification of Component MS-Storage.
In order to verify timeliness QoS for each component, Statechart must to be translated into a network of timed automata

and also timeliness QoS is converted into test automata.
Figure 13 depicts translated result of on part in Fig.12.
The translating times are summarized as follows.
Translation time
: 1153 ms
The number of states(before) : 89
The number of states(after): 179
entry?
tr:=tr+1
MS-out!
T:=0

T>2

The method can be applied to a design with complex connection of components.
Future works include simultaneous verification of several
kinds of timeliness QoS, and utilization of feedback information such as verification counter-examples.
Acknowledgement
This work is being conducted as a part of Stage Project, theDevelopment of Next Generation IT Infrastructure, supportedby Ministry of Education, Culture, Sports, Science and Technology.

error!

REFERENCES

MS-in!
T:=0

T<=2

exit?
tr:=tr-1

Figure 13: An UPPAAL Timed Automaton of Component
MS-Storage
For every component and for every timeliness QoS, verification is performed. The total CPU time is about one seconds.
We found that for every component, the verification is performed within a few seconds with UPPAAL, without state explosion. Also we found that there is no deadlock.

5.4 Discussion
Table 1 shows that when we perform the experiment withnine test automata, it outputs the correct result. The result of
Tab.2, however, shows that we cannot obtain the correct result until the number of test automata increases to 30. When
we perform the experiment with 30 test automata, the CPU
time increases exponentially. Therefore, we can conclude
that there is a trade-off between degree of precision and CPU
times. As shown in both tables, the CPU times of the experiments with 30 test automata are too large. Thus, as we
consider the trade-off, in this experiment, the trade-off point
is at which the number of process is 15.
Though we cannot exhibit that our proposed method is better than that of linear programming based method with respect
to the CPU time, the performance of the proposed method
is within useful reasonable time. The linear programming
method has many constraints on configuration, while the new
proposed method is flexible and is able to apply recursively
along with component hierarchy, which are the advantage ofthe proposed method.
Our proposed method has more acceptable inputs than theformer method. The difference between this and that of general class is very small. It is although not faster than the former method, it is more flexible than the former method.

6 Conclusions
This paper proposed a stepwise verification method for design of real-time system with UML/OCL focusing on timeliness QoS aspects. The method uses abstract QoS timed automata in order to reduce the possibility of state explosion.

[1] R. Staehli, F. Eliassen, J. Aagedal and G. Blair “Qualityof Service Semantics for Component-Based Systems,”
2nd Int’l Workshop on Reflective and Adaptive Middleware Systems, pp.153-157, 2003
[2] R. Alur and D.L. Dill: “A Theory for Timed Automata,”
In Theoretical Computer Science 125 pp.183-235, 1994.
[3] L. Ageto, P. Bouyer, A. Burgueño and K. G. Larsen:“The Power of Reachability Testing for Timed Automata,” LNCS, Vol.1530, pp.245-256, 1998.
[4] A. David and M. O. Möller: “From HUPPAAL to UPPAAL: Translation from Hierarchical Timed Automata
to Flat Timed Automata,” BRICS Technical Report Series, RS-01-11, 2001.
[5] H. Bowman, G. Faconti and M. Massink: “Specificationand verification of media constraints using UPPAAL,”In Proceedings of Design, Specification and Verificationof Interactive Systems’98, pp.261-277 Springer, 1998.
[6] K. Havelund, A. Skou, K. G. Larsen and K. Lund: ”Formal Modelling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using UPPAAL,” In Proceedings of the 18th IEEE Real-Time Systems Symposium, pp.2-13, 1997.
[7] Object Management Group:
Unified Modeing
Language Specification version 2.1, available at
http://www.omg.org/.
[8] B. Bordbar, J. Derrick and A. G. Waters: “A UML
approach to the design of open distributed systems,”
In Chris George and Huaikou Miao, editors, Formal
Methods and Software Engineering, LNCS, Vol.2495,
pp.561-572, 2002.
[9] UML Profile for Modeling Quality of Service and Fault
Tolerance Characteristics and Mechanisms, Request for
Proposal, available at http://www.omg.org[10] B. Bordbar and K. Okano, “Verification of Timeliness QoS Properties in Multimedia Systems,” 5th International Conference on Formal Engineering Methods(ICFEM ’03), LNCS 2885, pp.523-540, 2003[11] Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, PaulPettersson, and Wang Yi: “UPPAAL . a Tool Suite for
Automatic Verification of Real-Time Systems,” LNCS,
Vol.1066, pp.232-243, 1995.
[12] D. Akehurst, J. Derrick, and A. G. Waters: “Design
and Verification of Distributed Multi-media Systems,”
LNCS, Vol.2884, pp.276-292, 2003.

[13] The official OMG SysML site,
http://www.omgsysml.org/[14] J. Carlson, J. Håkansson and P. Pettersson: “SaveCCM:
An Analysable Component Model for Real-Time Systems,” Proc. of FACS’05, Electronic Notes in Theoretical Computer Science, Vol.160, pp.127-140, 2005.
[15] E. Nagai, A. Makidera, K. Okano, K. Taniguchi: “A
Method to Develop Distributed Real–Time Applications
Based on UML/OCL (in Japanese),” In the IEICE Transactions, Vol.J89-D No.4, pp683-692, 2006.