This tutorial is a step-by-step description of the process of creating a CATS model and performing
its analysis. Following this tutorial will show how easy CATS makes it to go from a simple model
definition to obtaining task response times. Additional sections will also show how to analyse systems
with feedback loops, simulate timed automata models and configure the CATS tool.
Creating a Model
Open Real-Time Modeling perspective.
Choose Real-Time Modeling and press OK.
Create a new CATS project in the workspace, select New->Project...
Expand Real-Time Modeling and choose Cats Project and press Next.
Enter "My Project" in the Project name box and press Finish.
Right click on the project name and select New->Other...
Expand Real-Time Modeling and select Components File and press Next.
Specify the name of a components file and press Finish.
Edit the my.components file as shown in the figure and press Ctrl-S (save).
Now we need to create timed automaton named MyTransformer.
Modeling with Timed Automata
Right click on the project name and select New->Other...
Expand Real-Time Modeling and select Timed Automata File and press Next.
Specify the name of a timed automata file and press Finish.
Expand the palette in the TA Editor and select Template.
Create a template by clicking in the upper left corner and dragging to the lower right corner.
Assign a name to the TA template by clicking once on its title bar, entering "MyTransformer" and finalising with Ctrl-Enter.
By using Location and Transition tools and the properties view specify the following timed automaton.
Double click the automaton title to open the declarations editor and enter the following line.
Close the declarations editor saving changes and define the template parameter as follows. Then, save my.ta file.
We are now ready to perform timing analysis.
Analysing Response Times
Open Performance Analysis perspective.
Choose Performance Analysis and press OK.
Click on a small triangle pointing downwards right to the Debug button and select Debug...
In the Debug configuration dialog specify the name of the configuration, choose my.components file as input, select "Uppaal Engine 4.0.0" in the Uppaal engine combo box and press Debug.
After analysis termination the screen should look similarly. The curves in RTC Plot show the results of the last analysis
step. Red lines correspond to task release (light red) / finish (dark red) events and blue lines denote available (light blue)
/ remaining (dark blue) computational resources. The Console view shows the steps taken by the tool during analysis.
You can navigate to any step in the Debug view and explore the segments of curves in the Variable view. During the MY.TRANSFORMER(INPUT)
step the tool used Uppaal engine to obtain approximated output of the TRANSFORMER process. The measurements taken to obtain
upper and lower bound curves are shown as yellow dots in the RTC Plot view.
If you click on MY.T1 step in the Debug view you will get the results of response time analysis for the task T1 in the Variables view.
Task T1 is schedulable because it's worst case response time is less than its relative deadline (5.5<6) and it always
has enough computational resources. The ready queue size for this task in the OS scheduler must be of size 12 though
sometimes its utilisation can be as few as 3 instances. The best case response time for the task T1 is 4.3.
Systems with Feedback
Open the fixedpoint.components system in the CATS Examples project. It consists of two tasks TASK1 and TASK2. The finishing
of TASK1 triggers the release of TASK2. The CPU is given to TASK2 first meaning that TASK2 has higher priority than TASK1
(fixed priority preemptive policy). The finishing of TASK2 in its turn releases the next instance of TASK1. Here we have
a feedback loop that connects the output of the system with its input. An initial condition (IN) is specified for the release
stream of TASK2.
Run the performance analysis for the fixedpoint system. It will terminate in 9 iterations. In the first iteration the tool
will apply initial condition as a release pattern for TASK2. Then it will compute the output of TASK2 and the CPU left for
the TASK1. After that AND operator can be applied and TASK1 can be computed. The analysis continues until the inputs of
all the TASKS in the system stabilise (become the same as on the previous iteration).
Even though the termination of the fixed point computation is not guaranteed in general, for some systems it is possible
to compute the fixed point solution.
Modeling Language
The modeling language of the CATS tool is a script-like language describing hierarchical topology of the system components,
their input/output ports, links connecting ports and entities associated with the components (timed automata, RTC functions,
abstract streams). The BNF grammar of the modeling language syntax is as follows:
COMPONENT ::= "component" <id> "{" COMPONENT | PORT | CONNECTION
| PROCESS | FUNCTION | TASK | STREAM
| PJD | BANDWIDTH | BDELAY | PERIODIC | TDMA
"}"
PORT ::= ("input" | "output") "port" <id> ( "," <id> )*
CONNECTION ::= TERMINAL ( "->" TERMINAL )+
TERMINAL ::= "null" | ( <id>
( ( "." <id> )
| ( <id> "(" TERMINAL ( "," TERMINAL )* ")" )
)
)
PROCESS ::= "process" <id> ( "," <id> )* "{" ( TEMPLATE | PORT )+ "}"
FUNCTION ::= "function" <id> "(" <id> ( "," <id> )* ")" "{" ( FUN_BODY )+ "}"
FUN_BODY ::= <id> "=" EXPRESSION
EXPRESSION ::= (( "add" | "sub" | "max" | "min"
| "maxPlusConv" | "maxPlusDeconv" | "minPlusConv" | "minPlusDeconv"
) "(" EXPRESSION "," EXPRESSION ")"
) |
(( "ceil" | "floor" ) "(" EXPRESSION ")"
) |
(( "scale" | "move" ) "(" EXPRESSION "," <real> "," <real> ")"
) | CURVE_REF
CURVE_REF ::= <id> "." ( "upper" | "lower" )
TASK ::= "task" <id> "[" <long> <long> <long> "]"
STREAM ::= "stream" <id> "{" ( "upper" CURVE | "lower" CURVE )+ "}"
CURVE ::= "{" ( "discrete" "[" <long> "]" ( <long> <long> )+ )
| ( <real> <real> <real> )*
( "periodic" "[" <real> <real> <long> <real> "]"
( <real> <real> <real> )+
)?
"}"
PJD ::= "pjd" <id> "[" <long> <real> <real> "]"
BANDWIDTH ::= "bandwidth" <id> "[" <real> "]"
BDELAY ::= "boundeddelay" <id> "[" <real> <real> "]"
PERIODIC ::= "periodic" <id> "[" <real> <long> <real> "]"
TDMA ::= "tdma" <id> "[" <real> <long> <real> "]"
<id> ::= LETTER ( LETTER | DIGIT | "_" )*
LETTER ::= [ "a"-"z" , "A"-"Z" ]
DIGIT ::= [ "0"-"9" ]
The main building blocks of the Cats model are components. They interact with each other
via connections that link component ports. Ports represent interfaces of components. There
are two types of components - high level and low level. High level components can build
hierarchical structures and contain other high or low level components. High level components
may have an arbitrary number of ports. Low level components cannot contain other components.
The low level components are: processes, functions, tasks, and streams.
Ports have a name and the direction (input or output). Connections always origin in an
output port and end up in an input port. Functions and streams are special case of
components; they do not have output ports but rather act as output ports themselves.
A process component is defined by single timed automaton specified using "template"
keyword. All the synchronization actions (e.g.
a!
or
a?
) of
the timed automaton must be declared as input (
a?
) or output (
a!
)
ports of the process component.
Function components allow to define functions consisting of
Real-Time Calculus (Thiele et.al.) basic and
complex operations on curves. The input ports of a function component correspond to
the parameters of the function that the component defines. Functions are described as
a list of expressions.
Task components are used to model execution of real time tasks on a processing unit.
Every task component is parameterized with the best and the worst execution time, deadline,
and has four predefined ports: input -
release
and
demand
, and
output -
finish
, and
rest
. They correspond respectively to the
task arrival pattern, the resource available for the task computation, the task finish
pattern and the remaining computational resource.
A stream component statically defines an abstract stream by a pair of curves representing
its upper and lower bounds. Stream may represent data, event or resource flows in the
system. There are three ways a stream can be specified: an aperiodic set of segments, a
pair of sets of segments representing periodic and aperiodic parts, and a discrete
periodic curve.
In the first case the curve is a list of triples of numbers denoting the start
coordinate (integer) and the slope (real) of the segments.
In the second case a special term
periodic [px0 py0 period pdy]
can be
inserted anywhere in the list of curve segments. It defines the square area with the
bottom left corner
(px0,py0)
and the size
(period,pdy)
. The
segments to the left of the term are considered as periodic and to the right - as
aperiodic parts respectively.
A discrete periodic curve has the step nature and defined using the
discrete[period]
term specifying the period and a set of pairs of integer
numbers representing left coorinates of the discrete steps.
Special streams
pjd, bandwidth, boundeddelay, periodic,
and
tdma
are ported from the
Modular
Performance Analysis package of
Real-Time Calculus Toolbox.
Configuring the Tool
Open the preferences dialog by selecting Window->Preferences...
Expand Cats and select Engine Sites. Here you can configure the Uppaal verification engine.
Choose the locality of the engine (local or remote), fill in corresponding boxes, specify
the type of the engine and how many processors the engine may occupy on your computer.