This page’s menu:

Online Documentation

Visit docs.uppaal.org for online documentation.

Presentations

Tutorials

External Contributions

Frequently Asked Questions

In this section we collect frequently asked questions (and answers) about Uppaal.

  1. How do I get started with Uppaal?
    The are some tutorials to get you started.
    You should also study the examples in the demo folder of Uppaal installation, read the documentation.

  2. uppaal.exe says “This application requires a Java Runtime Environment 11.0-21.0” even though Java is already installed, why?
    This application requires a Java Runtime Environment 11.0-21.0
    The issue is that the installed Java Runtime has not been registered in JavaSoft folder of the Windows Registry. In case of Adoptium distributions JRE registration is optional and need to be enabled during the installation step:
    JavaSoft (Oracle) registry keys

  3. Can I save Uppaal models in a textual format?
    Yes, Uppaal supports .xta-format where the graphical part is saved separately in .ugi file. Choose Save As... and enter a filename with .xta extension, click Save.

  4. How do I run Uppaal 4.0 in compability mode?
    There is a mode for compability with Uppaal 3.4, which can be enabled by defining the environment variable UPPAAL_OLD_SYNTAX. Set the variable to any value, and restart Uppaal for the setting to take effect. Remove the variable from the environment to get back to normal 4.0 operation.

  5. Will I be able to use system descriptions stored in .ta- or .atg-format in Uppaal?
    .ta- and .atg-files are old file formats used in earlier versions of Uppaal. The current file format, used since version 3.2, is based on XML and uses the extension .xml. Version 3.0 included a conversion tool from .atg-files to .xta format used in that version. The current version can open .ta- and .xta-files directly, use Open System in the File menu. Since version 3.4 the standalone verifier verifyta is able to read .ta-, .xta- and .xml-files directly.

  6. Can Uppaal save system descriptions in .ta- or .atg-format?
    No, since version 3.4 there is no support in Uppaal for saving .ta- or .atg-files.

  7. Can system descriptions and system requirements created in GUI be analysed with the stand-alone verifier verifyta?
    Yes, verifyta can handle files in the .ta-, .xta- and .xml-formats as well as the .q-format.

  8. What is the semantics of urgent locations?
    The semantics of an urgent location is the same as: introducing a new clock; reset the new clock on all in-going transitions to the location; and add a conjunct to the location invariant requiring the new clock to be <=0. Intuitively, this forces the process to leave an urgent location without delay.

  9. How do I run the GUI locally connected to a remote verification server?
    Assuming that the verification server is running on machine with IP address w.x.y.z and listening for connection socket on port 2350, use the command uppaal --serverHost w.x.y.z --serverPort 2350.
    Starting with version 5, the engine can be configured in the Edit menu.

  10. How do I start a verification server that accepts remote connections?
    Run the socketserver with no arguments to start a server that accepts remote connection on socket port 2350. Use the command line option -p to configure the server to listen on another port. The socketserver is only availabe on Linux and macOS.
    Note: there is no authentication performed, meaning that anybody aware of the running server, can connect to it. The server may also be vulnerable to attacks.
    Starting with version 5, the remote engine can be starting through ssh command, which is more secure.

  11. When loading a project, I get the error message Could not connect to server. What’s wrong?
    First, check the status log on the verification tab in the GUI. It might contain additional information. If you are using a remote verification server, see the entries about remote servers.
    If you are running with a local verification server check that the GUI can find the server executable and that you have permisson to execute the server binary. If you are using Linux or macOS you may also try to execute the verification server manually from the command prompt. See the above answers on how to do this. If you use the default port of 2350 and execute the GUI and verification server on the same host, you do not need to add additional options when starting the GUI.

  12. I try to run Uppaal in Windows by clicking on the file uppaal.jar, but WinZip or other archive program gets opened instead. How do I run Uppaal in Windows?
    It seems that another program has “stolen” the file association for jar files. You can either try to recreate the file association for jar files (it should run with javaw -jar) or simply reinstall Java.

  13. How do I produce colored .eps-files of an automaton?
    Normally, Uppaal produces gray-scale eps-files. It is possible to instruct the tool to generate colored eps-files by using the command line option -psColors on.
    To produce an eps-file of a template, use item Save Postscript of the Templates menu.
    To produce an eps-file of a process as shown in Simulator, right-click on the process in Simulator and choose Export from the pop-up menu.

  14. How do I force Uppaal’s GUI to use a specific language?

    • Linux (from 4.0.7+): use LANG=[code] ./uppaal, where code is the language code of a supported language (currently en, zh, ja, da, lt, ru). If the environment defines the LANG variable to follow some standard it will also work, like ja_utf8.
    • Windows: make a shortcut to uppaal.jar, edit the command of the shortcut to java -Duser.language=[code] -jar <path to uppaal.jar>.

  15. How do I export and interpret the traces from Uppaal?
    There are four ways of extracting the traces:

    • Textual format: use command line utility verifyta to produce the trace in human-readable state-transition format. The utility is distributed together with Uppaal and found in a bin-* directory. Type verifyta -h inside shell (cmd.exe on Windows) to see further options.
    • C/C++ API: export the trace as .xtr file and then interpret it with tracer utility from tracer repository.
    • Java API: use model.jar library included in lib folder of Uppaal distribution. The java-doc is included in lib/model-javadoc.jar and thus can be imported into IDEs such as Eclipse and Netbeans. Uppaal distribution also includes demo/ModelDemo.java code showing how to manipulate the model, import, export traces and how to interact with simulator and model-checking APIs of the engine.
    • Java Plugin API: integrated tab can access models and traces from within Uppaal, see uppaal-plugin-demo.

  16. Running Uppaal on Mac OS X I get the error java.io.FileNotFoundException: /Volumes/uppaal/UPPAAL.app/Contents/Resources/Java/license.txt (Read-only file system). What is the problem?
    You are probably running Uppaal from a dmg image file. Please move the content of the dmg file to a readable disc, e.g. to your /Applications directory on your system volume, or a directory on your Desktop.

  17. How do I use Uppaal through a proxy?
    If you are using Windows. Locate the installation directory of Uppaal. Create a shortcut to uppaal.jar and give it the name you want. Edit the shortcut and change the command line used. You should see java -jar "C:\...\uppaal.jar". Change it to

    java -DproxySet=true
-Dhttp.proxyHost=proxyhostURL
-Dhttp.proxyPort=proxyPortNumber
-Dhttp.proxyUser=someUserName
-Dhttp.proxyPassword=somePassword
-jar "C:\...\uppaal.jar"

    where you fill in the information concerning your proxy. You need to enter your user name and password only if you need to login on the proxy, otherwise remove the two corresponding definitions.

    If you are using Linux or macOS. Locate the installation directory of Uppaal. Edit the script uppaal and add

    -DproxySet=true \
-Dhttp.proxyHost=proxyhostURL \
-Dhttp.proxyPort=proxyPortNumber \
-Dhttp.proxyUser=someUserName \
-Dhttp.proxyPassword=somePassword

    to the JAVA_DEF default option definition at the beginning. The \ are here to break lines. Do no add any character after \. Fill the needed information on your proxy and remove the definitions for user name and password if they are not needed for your proxy.

  18. How do I fix damaged images under Mac OS X Lion?
    Actually the images are not damaged but the application gate keeper on Lion must be setup. Delete the images you have. Configure the gate. Then re-download the images and it will work.

  19. Why does Uppaal Simulator, Verifier, Server and/or Verifyta crash almost immediately on Linux?
    Possible cause: Uppaal cannot access a license in ~/.config/uppaal (Uppaal-5), uppaal-version.number/ (Uppaal-4), tries to fetch the license over the internet and create a file, but it fails in some step.
    Symptoms:

    • Running some old Uppaal version on a much newer Linux distribution.
    • Verification does not start and brings server connection lost instead (server crash).
    • verifyta and/or server does not start but says “internet connection required for activation”
    • Older 32bit releases (TIGA, ECDAR) are being run on 64bit Linux distribution.
    • Diagnostic runs with strace server finish with lots of “file not found” messages upon looking up 32bit libraries like /lib32/libc6.so, /usr/lib/libnss.so and so on.

    Possible fixes:

    • Make sure that the computer has a working internet connection, e.g. check with a commands ping uppaal.veriaal.dk and ping bugsy.grid.aau.dk, inspect the network interface (use command ifconfig or ipconfig).
    • Make sure that the Uppaal-5 configuration folder ~/.config/uppaal has write permissions, e.g. use ls -ld ~/.config/uppaal command to inspect the permissions, touch ~/.config/uppaal/test.txt should succeed.
    • Make sure that the Uppaal-4 installation folder has write permissions, e.g. use ls -ld . command to inspect the permissions, touch license.txt should succeed inside the Uppaal-4 installation directory.
    • When using 32bit Uppaal on 64bit Linux host, install 32bit libc library to enable networking support for 32bit binaries, e.g. sudo apt-get install libc6:i386 (you may need to enable i386 architecture in /etc/apt/sources.list, sudo apt-get update and then sudo apt-get install libc6:i386).
    • See Help/About menu for version and build date information, copy the library files mentioned in strace server output from a corresponding Ubuntu LTS release. Alternatively contact us and/or post an issue on github issue tracker or github discussions. Note the Uppaal version and the operating system version.

  20. Floating point variables and operations are ignored in symbolic queries, Symbolic Simulator or the verification of such queries crash the engine, why?
    Floating point operations are not supported by the symbolic analysis (only integers are allowed). The only valid use of floating point operations is when they are used to model dynamical cost and does not influence the behavior of the model, i.e. the floating point operations can be safely abstracted away.
    Dynamical cost can be modeled using hybrid clock variables using floating point operations which have effect in SMC and Stratego queries.

  21. How to fix “Internal Error” “Zero length string passed to TextLayout constructor”?

    The issue is triggered by empty lines (“zero length string”) in the timed automata labels when they are being rendered by Java 11 on Windows.
    The solution is to upgrade to the next long term support Java release, at least 17.

  22. When started on a command line, Uppaal produces the following warnings:

    WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.uppaal.gui.Main (file:/opt/local/uppaal-4.1.24/uppaal.jar) to field sun.awt.X11.XToolkit.awtAppClassName
WARNING: Please consider reporting this to the maintainers of com.uppaal.gui.Main
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release

    These warnings are harmless and can be ignored.
    The reason is that Uppaal is trying to set the application name for the Window Manager to display in the application bar, but it is using the internal Java API to achieve it. Java detects and warns against it because internal API does not have any guarantees for continued support. Unfortunately, Java does not provide a standard way of setting the application name to be shown in all possible Window Managers.

  23. Why Uppaal window is blank with no errors when running on non-reparenting window manager like Sway and bspwm?
    This seems to be a problem with Java AWT when running under non-reparenting Linux window managers.
    To fix this, set the environment variable _JAVA_AWT_WM_NONREPARENTING=1.

Published Material

Incomplete list of publications related to Uppaal.

UPPAAL CORA

2005

2004

2003

2002

2001

2000

1999

TRON

  1. Online Testing of Real-time Systems. Marius Mikučionis. Ph.D. thesis preprint. Department of Computer Science, Aalborg University. May 10, 2010. (bib, pdf)
  2. Testing Real-Time Systems Using UPPAAL. Anders Hessel, Kim G. Larsen, Marius Mikučionis, Brian Nielsen, Paul Pettersson and Arne Skou. Formal Methods and Testing. Springer Berlin / Heidelberg. April 13, 2008. (bib, pdf, doi)
  3. Testing Real-time Embedded Software using UPPAAL-TRON - An Industrial Case Study. Kim G. Larsen, Marius Mikučionis, Brian Nielsen, Arne Skou. The 5th ACM International Conference on Embedded Software. Jersey City, NJ, USA. September 18-22, 2005. (bib, pdf, models)
  4. T-UPPAAL: Online Model-based Testing of Real-time Systems, tool demo. Marius Mikučionis, Kim G. Larsen, Brian Nielsen. 19th IEEE International Conference on Automated Software Engineering, 396-397. Linz, Austria. September 24, 2004. (bib, pdf)
  5. Online Testing of Real-time Systems using Uppaal: Status and Future Work. Kim G. Larsen, Marius Mikučionis, Brian Nielsen. Dagstuhl Seminar Proceedings volume 04371: Perspectives of Model-Based Testing. Schloss Dagstuhl, Wadern, Germany. September 5-10, 2004. (bib, pdf, doi)
  6. Online Testing of Real-time Systems Using UPPAAL. Kim G. Larsen, Marius Mikučionis, Brian Nielsen. Formal Approaches to Testing of Software. Linz, Austria. September 21, 2004. (bib, pdf, doi)
  7. Online On-the-Fly Testing of Real-time Systems. Marius Mikučionis, Kim G. Larsen, Brian Nielsen. Basic Research In Computer Science Report Series. Aalborg, Denmark. December, 2003. ISSN 0909-0878. (bib, abstract, pdf)
  8. Real-time System Testing On-the-fly. Marius Mikučionis, Brian Nielsen, Kim G. Larsen. The 15th Nordic Workshop on Programming Theory. Turku, Finland. October 29-31, 2003. (bib, pdf)
  9. On-the-fly Testing Using Uppaal. Marius Mikučionis, Eglė Sasnauskaitė. Master thesis, Department of Computer Science, Aalborg University. June 11, 2003. (bib, pdf)