| Line 1... |
Line 1... |
Author: T. Bourke (CSE/NICTA UNSW)
|
Urpal
|
|
-----
|
This software is a prototype only. It most likely contains undiscovered
|
Urpal is your pal for Uppaal.
|
faults. Caveat Modellor.
|
|
|
Urpal takes an Uppaal model as input, performs manipulations as described by
|
One good sanity check is to check trace inclusion of a model with itself,
|
a simple command language, and writes the resulting model back to a file.
|
i.e. given AUTO, construct AUTO' then check:
|
Its prime feature is the ability to construct a testing automaton for
|
AUTO || AUTO' |= A[] not AUTO'.Err
|
determining trace inclusion for a restricted class of timed automata. Uppaal
|
A failure can indicate a bug in urpal, or an initial model that is not
|
can also: duplicate automata; create automata ready to accept all
|
deterministic. The sanity check can be passed even if, or because, AUTO'
|
synchronisations on a set of channels; prune transitions based on their
|
refuses to participate in an action with AUTO. This should never happen if
|
action label; conflate, drop and rename locations; and scale the graphical
|
the construction is performed correctly; it would indicate a bug in urpal.
|
layout of a model. More details are in the manual_page.
|
Running a simulation can increase confidence in AUTO'.
|
|
|
Descriptions of the testing construction can be found in:
|
The layout routines do not give perfect results, but they usually make the
|
|
|
* The thesis of Mariëlle Stoelinga, specifically Chapter 7 and Appendix
|
|
A. Development on Urpal began from her descriptions at the suggestion
|
|
of Frits Vaandrager.
|
|
|
|
* The Scaling_up_Uppaal paper of Henrik Ejersbo Jensen, Kim Guldstrand
|
|
Larsen, and Arne Skou. Urpal incorporates their construction for
|
|
handling urgent locations and shared variables.
|
|
|
|
* The paper by Arcot Sowmya and me, to be presented at EMSOFT 2008. This
|
|
paper presents several improvements to the original CSE technical
|
|
report (UNSE-CSE-TR-0723).
|
|
|
|
The testing construction cannot be performed on all timed automata,
|
|
specifically several modelling features are not supported:
|
|
* non-deterministic automata (this assumption is not checked),
|
|
* non-synchronizing (τ) transitions,
|
|
* committed locations,
|
|
* process priorities,
|
|
* channel priorities,
|
|
* inputs on broadcast channels,
|
|
* some combinations for forall and select bindings (see this paper).
|
|
|
|
The software was developed at the The University of NSW and NICTA. It is
|
|
released under a BSD License. Urpal uses technology developed with the
|
|
imagination and ideas from NICTA, Australia's ICT Centre of Excellence. The
|
|
source repository can be browsed online.
|
|
|
|
This software is provided as a prototype only: use at your own risk! It surely
|
|
contains faults, please report them.
|
|
|
|
Graphviz is required to run Urpal. The source code has additional
|
|
compilation dependencies.
|
|
|
|
Step-by-step Example
|
|
--------------------
|
|
1. Download and extract Urpal.
|
|
|
|
2. Download the Uppaal DTD, flat-1_1.dtd.
|
|
|
|
3. Install Graphviz if necessary.
|
|
|
|
4. Edit urpalrc, setting the paths to flat-1_1.dtd and Graphviz:
|
|
|
|
dtd_path="flat-1_1.dtd"
|
|
graphviz {
|
|
path = "/usr/local"
|
|
engine = neato
|
|
}
|
|
|
|
Urpal will look for the Graphviz executables, like fdp and neato, in a
|
|
bin subdirectory of the path given.
|
|
|
|
5. Download the simple example model:
|
|
http://www.cse.unsw.edu.au/~tbourke/software/urpal-example.xml.
|
|
|
|
6. Start a terminal, and run urpal:
|
|
./urpal -i urpal-example.xml -o urpal-example-after.xml - e "Test=maketest(Template)"
|
|
|
|
In the Windows command interpreter (cmd.exe), type rather:
|
|
urpal -i urpal-example.xml -o urpal-example-after.xml -e "Test=maketest(Template)"
|
|
|
|
7. The program should produce a model urpal-example-after.xml that can be
|
|
opened in Uppaal. The new model should contain the original Template
|
|
automaton and a new Test automaton.
|
|
|
|
One good way to verify the result is to model check the original automaton
|
|
against the generated test automaton, which also exposes models that are not
|
|
deterministic. This would be done for the above example by first changing
|
|
the system declaration to: system Template, Test;, then verifying the
|
|
formula: A[] (not Test.Err). Such tests have previously revealed faults in
|
|
Urpal. Another test is to verify that no new deadlocks are introduced, as
|
|
Test automata are always ready to synchronize. Since there are already two
|
|
possibilities for deadlock in the example, the formula is:
|
|
A[] (deadlock imply ((Template.s2 and Template.x >=3 and Template.x < 4)
|
|
or Template.s3))
|
|
|
|
The source repository includes a number of small test models, and a larger
|
|
railway crossing controller example.
|
|
|
|
Improving the appearance of results
|
|
-----------------------------------
|
|
The layout routines rarely give perfect results, but they usually make the
|
basic structure clear enough so that sense can be made of counter-example
|
basic structure clear enough so that sense can be made of counter-example
|
traces, and they are a reasonable starting point for manual rearrangement
|
traces, and they are a reasonable starting point for manual rearrangement of
|
of label positions (the transition nails make other changes painful). If the
|
label positions (the transition nails make other changes painful). If the
|
results are very poor, try:
|
results are very poor, try:
|
* using scale() to enlarge the source model before generating the tester
|
|
* using tabulate(<tester>, {Err}) to organize labels differently
|
|
* try both fdp (graphviz { engine=fdp }) and neato (graphviz { engine=fdp })
|
|
|
|
The program works best under unix, but it will also function under Cygwin.
|
|
|
|
Bugs may be reported to tbourke@cse.unsw.edu.au
|
|
|
|
T. Bourke (CSE/NICTA UNSW).
|
|
2007-12-05
|
|
|
|
Initial Configuration
|
|
---------------------
|
|
1) Install Graphviz.
|
|
The program will work without Graphviz, although it will complain
|
|
often and most automatic layout features will be disabled.
|
|
|
|
Under windows, the program has been tested against the normal version
|
|
of Graphviz (not a version specially compiled for Cygwin).
|
|
|
|
2) Download flat-1_1.dtd:
|
* Scaling the source model before generating the test automaton. For
|
http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd
|
example, Test=maketest(scale(Template, 2.0)).
|
|
|
3) Edit two entries in urpalrc:
|
* Tabulating the labels on transitions to the error state. For example,
|
dtd_path should point to flat-1_1.dtd
|
Test=tabulate(maketest(Template), {Err}).
|
graphviz/path should point to the graphviz installation
|
|
directory (which has a bin/ subdirectory)
|
|
|
|
Running the program
|
* Trying different Graphviz layout routines. For example, either fdp --
|
-------------------
|
set=graphviz{engine=fdp} or the other spring-based approach neato --
|
1) Listing templates in an Uppaal model:
|
set=graphviz{engine=neato}. Usually one will give better results than
|
urpal -i limitedbind.xml -e show
|
the other for a particular model.
|
|
|
2) Creating the testing construction:
|
* Various combinations of the above.
|
urpal -i limitedbind.xml -o test.xml -e 'TEST=maketest(Template)'
|
|
|
|
3) If the result is hard to read, try variations of:
|
* Ultimately, manual rearranging the original automaton or the resulting
|
urpal -i limitedbind.xml -o test.xml -e 'TEST=tabulate(maketest(scale(Template,2.0)),{Err})'
|
test automaton is sometimes the only satisfactory approach. Scaling the
|
|
model and using the tabulate feature can make it easier.
|
|
|
Further commands and options are listed in the included documentation.
|
Author: Timothy Bourke
|
|
LastChangedDate: 2008-08-28 11:58:27 +1000 (Thu, 28 Aug 2008)
|
|
|
|
|