Presentations
- Timed and Hybrid Systems in Uppaal2k, by Kim G. Larsen and Paul Pettersson, presented at MOVEP'2k, June 21, 2000. (html, ps.gz, pdf).
- Uppaal2k, by Paul Pettersson and Kim G. Larsen, in Bulletin of the European Association for Theoretical Computer Science, volume 70, pages 40-44, 2000. ( .ps.gz, .pdf, bibtex ).
- Uppaal pamphlet (concise), ( PDF),
- Formal Methods for Real Time Systems: Automatic Verification & Validation, by Kim G. Larsen. Slides describing Uppaal and formal methods for real-time systems in general. Presented at the ARTES summer school, August 1998.
Tutorials
- Timed Automata: Semantics, Algorithms and Tools. [BW04].
- Uppaal SMC Tutorial. Reformatted version of [DLLMP15]. Example models:
- Custom delay distribution for Section 7.2.
- Tutorial on Uppaal. Revised and extended version of [BDL04]. This document is updated (see date on first page).
- Uppaal in a Nutshell [LPW97b].
- Uppaal 4.0: Small Tutorial. A short description of the tool as well as some examples. (pdf).
- Translated to Japanese, thanks to T. Fujikura and Kiyomi Hirano (pdf). Outdated version
- How to typeset Uppaal code in Latex, by Marius Mikucionis.
External Contributions
- UrPal — plugin for checking most common modeling mistakes.
- uppaal-ecore-parser — parser for plain-text UPPAAL files to Ecore models.
- EMF-based tooling — meta-model and tools for Eclipse frameworks.
Frequently Asked Questions
In this section we collect frequently asked questions (and answers) about Uppaal2k.
- How do I get started with Uppaal?
The are some tutorials to get you started. You should also study the examples in the demo directory, created during the installation, and read the documentation available from the Help menu in Uppaal. - 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 variableUPPAAL_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. - 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 verifierverifyta
is able to read .ta-, .xta- and .xml-files directly. - 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. - 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. - 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. - How do I run the GUI locally connected to a remote verification server?
Assuming that the verification server is running on machine xxx.yyy.zzz and listening for connection socket 2350, use the command "uppaal2k -serverHost xxx.yyy.zzz -serverPort 2350
". - How do I start a verification server that accepts remote connections?
Run thesocketserver
with no arguments to start a server that accepts remote connection on socket 2350. Use the command line option-p
to configure the server to listen on another socket. Thesocketserver
is only availabe on Linux and SunOS.
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 acodeacks. - 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 Solaris 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. - I try to run Uppaal in Windows
by clicking on the file uppaal.jar, but WinZip is opened
instead. How do I run Uppaal in
Windows?
It seems that winzip has "stolen" the file association for jar files. You can either try to fix the file association for jar files (it should run 'javaw -jar') or simply reinstall java. - 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 the simulator), use Save Postscript in the pop-up menu of the process (activate the pop-up menu by right-clicking the process in the simulator). - How do I force Uppaal's GUI to use a
specific language?
- Under Linux (from 4.0.7 & current internal dev version):
use
LANG=[code] ./uppaal
, wherecode
is the language code of a supported language, currentlyen, zh, ja, da, lt, ru
. If the environment defines the LANG variable to follow some standard it will also work, like ja_utf8.. - Under Windows: make a shortcut to
uppaal.jar
, edit the command of the shortcut tojava -Duser.language=[code] -jar <path to uppaal.jar>
.
- Under Linux (from 4.0.7 & current internal dev version):
use
- How do I export and interpret the traces from Uppaal?
There are three 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 abin-*
directory. Typeverifyta -h
inside shell (cmd.exe
on Windows) to see further options. - C++ API: export the trace as
.xtr
file and then interpret it withtracer
utility from UTAP library. - Java API: use
model.jar
library included inlib
directory of the Uppaal distribution. The java-doc is included inlib/model-javadoc.jar
and thus can be imported into IDEs such as Eclipse and Netbeans. Uppaal distribution also includesdemo/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.
- Textual format: use command line utility
- How do I switch to Java 6 on Mac OS X?
On Mac OS X 10.5 the default Java virtual machine is Java 5. To switch to Java 6, run/Applications/Utilities/Java/Java Preferences.app
and select Java 6. From version 4.0.7, Uppaal will not run on Mac OS X 10.4 and Java 6 is not available on that platform. - Running UPPAAL on Mac OS X I get the error
java.io.FileNotFoundExceptino: /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 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. - UPPAAL freezes on Mac, what do I do?/
On Lion or Mountain Lion, the GUI may freeze. Update your Java on this link. - You cannot install UPPAAL on Mac OS Lion or later.
- Delete the dmg file you downloaded.
- Open Preferences.
- Open Security and Privacy.
- Select "Allow applications downloaded from: " anywhere.
- Download UPPAAL again and install.
- 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 Mac. 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 theJAVA_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. - 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. - Why does UPPAAL simulator, verifier, server and/or verifyta crash almost immediately?
Possible cause: UPPAAL cannot access a license in
uppaal-version.number/license.txt
file, tries to fetch the license over the internet and create a file, but it fails in some step.Symptoms:
- Older 32bit releases (TIGA, ECDAR) are being run on new 64bit Linux host.
- Verification does not start and brings "server connection lost" instead.
verifyta
and/orserver
does not start but says "internet connection required for activation"- 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 command
ping bugsy.grid.aau.dk
, inspect the network interface (use commandifconfig
oripconfig
). - Make sure that the installation directory
uppaal-version.number
has write permissions, e.g. usels -ld .
command to inspect the permissions,touch license.txt
should succeed inside the UPPAAL installation directory. - 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 thensudo apt-get install libc6:i386
).
- Attempt to export graphical images results in internal error "org.freehep.graphicsbase.util.export.ExportFileType is not an ImageIO SPI class"
FreeHEP library is broken since Java 9. A workaround is to install and use Java 8.
- Floating point variables and operations are ignored in symbolic queries or the verification of such queries crash the engine
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 by
hybrid clock
variables using floating point operations which have effect in Stratego queries. - 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
The warning is 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 ≥9 implements checks for such access and warns against it because internal API does not have any guarantees for continued support. Unfortunately Java does not provide an alternative way of setting the application name.
Published Material
Incomplete list of publications related to Uppaal.
- [MMSTT19] Timed Automata Networks for SCADA Attacks Real-Time Mitigation, Fabio Martinelli, Francesco Mercaldo, Antonella Santone, Christina Tavolato-Wötzl, Paul Tavolato. ICSSA 2019: 5th International Conference on Software Security and Assurance, July 2019. (.pdf)
- [MMS19] Real-Time SCADA Attack Detection by means of Formal Method, Fabio Martinelli, Francesco Mercaldo, Antonella Santone. 28th IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE-2019), June 2019. (doi)
- [DLLMP15] Uppaal SMC Tutorial, Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen. International Journal on Software Tools for Technology Transfer (STTT), January 2015, Volume 17, Issue 4, pp 397-415. Springer Berlin Heidelberg. ISSN 1433-2787, 1433-2779. (doi, .pdf, .bibtex)
- [RSV11] Modelling and Verication of Web Services Business Activity Protocol A.P. Ravn, J. Srba, S. Vighio. In proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2010.
- [RVS10] A Formal Analysis of the Web Services Atomic Transaction Protocol with Uppaal. A.P. Ravn, S. Vighio and J. Srba. In Proceedings of the 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'10), LNCS, Springer-Verlag, 2010.
- [HP07] A Global Algorithm for Coverage-Based Test Case Generation. Anders Hessel and Paul Pettersson. Accepted for MBT 2007, Third Workshop on Model-Based Testing, March 31 - April 1, 2007, Braga, Portugal, Satellite workshop of ETAPS 2007
- [HP06] Model-Based Testing of a WAP Gateway: an Industrial Study. Anders Hessel and Paul Pettersson. In Proceedings of FMICS and PDMC 2006, LNCS 4346.
[DHLP06] Model Checking Timed Automata with Priorities using DBM Subtraction, Alexandre David, John Håkansson, Kim G. Larsen, and Paul Pettersson. In proceeding of the 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06).
[CHP05] SaveCCM: An Analysable Component Model for Real-Time Systems, Jan Carlson, John Håkansson, and Paul Pettersson. In proceedings of the International Workshop on Formal Aspects of Component Software (FACS'05). Electronic Notes in Theoretical Computer Science, Elsevier, 2005. ( doi:10.1016/j.entcs.2006.05.019 )
- [BAO05] An Evaluation Mechanism for QoS Management in Wireless Systems, B. Bordbar, R. Anane and K. Okano. In proceedings of the 11th International Conference on Parallel and Distributed Systems, ICPADS 2005 Vol.II pp.150-154. (.pdf)
- [BHJP04] Specifying and Generating Test Cases Using Observer Automata. Johan Blom, Anders Hessel, Bengt Jonsson, Paul Pettersson. In Proceedings of the 4th International Workshop on Formal Approaches to Testing of Software 2004 (FATES'04). ( abstract, bibtex )
- [HP04] A Test Case Generation Algorithm for Real-Time Systems. Anders Hessel and Paul Pettersson. In Proceedings of the Fourth International Conference on Quality Software 2004 (QSIC'04).
- [BW04] Timed Automata: Semantics, Algorithms and Tools, Johan Bengtsson and Wang Yi. In Lecture Notes on Concurrency and Petri Nets. W. Reisig and G. Rozenberg (eds.), LNCS 3098, Springer-Verlag, 2004. (ps)
- [BDL04] A Tutorial on Uppaal, Gerd Behrmann, Alexandre David, and Kim G. Larsen. In proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT'04). LNCS 3185. ( .ps.gz, .pdf, .bibtex )
- [HLNPS03] Time-Optimal Real-Time Test Case Generation using UPPAAL. Anders Hessel, Kim G. Larsen, Brian Nielsen, Paul Pettersson, and Arne Skou. In Proceedings of the 3rd International Workshop on Formal Approaches to Testing of Software 2003 (FATES'03).
- [BO03] Verification of Timeliness QoS Properties in Multimedia Systems, B. Bordbar and K. Okano. In proceedings of the 5th International Conference on Formal Engineering Methods (ICFEM 2003), LNCS 2885, pp.523-540. (.pdf)
- [DBLW03] Unification & Sharing in Timed Automata Verification, Alexandre David, Gerd Behrmann, Kim Guldstrand Larsen, Wang Yi. Accepted for presentation at SPIN Workshop 2003.(ps.gz, bibtex)
- [DBLW03] A Tool Architecture for the Next Generation of Uppaal, Alexandre David, Gerd Behrmann, Kim G. Larsen, and Wang Yi. Technical report Uppsala University 2003. ( .ps, .ps.gz, .pdf, abstract )
- [DMW03]Verification of UML Statecharts with Real-Time Extensions, Alexandre David, M. Oliver Möller and Wang Yi. Technical report Uppsala University 2003. ( .ps, .ps.gz, abstract )
- [LLPY03] Compact Data Structure and State-Space Reduction for Model-Checking Real-Time Systems, Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. In Real-Time Systems - The International Journal of Time-Critical Computing Systems, volume 25, issue 1, Kluwer Academic Publisher, 2003.
- [DMW02] Formal Verification of UML Statecharts with Real-Time Extensions, Alexandre David, M. Oliver Möller and Wang Yi. In Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, LNCS 2306, pages 218-232, Ralf-Detlef Kutsche and Herbert Weber (eds.). (.ps.gz, .pdf, abstract, bibtex)
- [BDKLLPY02] Automated Analysis of an Audio Control Protocol Using Uppaal, Johan Bengtsson, W. O. David Griffioen, Kåre J. Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. In Journal of Logic and Algebraic Programming, volumes 52-53, pages 163-181, Holger Hermanns and Joost-Pieter Katoen (eds.). July-August, 2002. (.ps.gz, .pdf, abstract, bibtex )
- [BBDLPY02] Uppaal Implementation Secrets, Gerd Behrmann, Johan Bengtsson, Alexandre David, Kim G. Larsen, Paul Pettersson, and Wang Yi. In Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), 2002. (.ps.gz, .pdf, abstract, bibtex)
- [DM01] From HUppaal to Uppaal: A Translation from Hierarchical Timed Automata to Flat Timed Automata, Alexandre David and M. Oliver Möller. Technical Report BRICS 2001 (.ps.gz, .pdf, abstract)
- [HLP01] Guided Synthesis of Control Programs Using Uppaal, Thomas Hune, Kim G. Larsen, and Paul Pettersson. In Nordic Journal of Computing (NJC), volume 8, number 1, 2001, pages 43-64. (ps.gz, pdf, abstract, bibtex)
- [BDLMPY01] Uppaal - Present and Future, Gerd Behrmann, Alexandre David, Kim G. Larsen, Oliver Möller, Paul Pettersson, and Wang Yi. In Proceedings of the 40th IEEE Conference on Decision and Control (CDC'2001). Orlando, Florida, USA, December 4 to 7, 2001. ( .ps.gz, .pdf, abstract, bibtex)
- [LPY01] Formal Design and Analysis of a Gear Controller, Magnus Lindahl, Paul Pettersson and Wang Yi. In Springer International Journal of Software Tools for Technology Transfer (STTT), volume 3, issue 3, pages 353-368, 2001. ( ps.gz, pdf, abstract, bibtex )
- [LBBFHPR01] As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata, Kim G. Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Pettersson, and Judi Romijn. In Procceedings of the 13th Conference on Computer Aided Verification, (CAV'01). 2001. LNCS 2102, pages 493-505, G. Berry, H. Comon, A. Finkel (Eds.). Paris, France, July 18 to 23, 2001. ( .ps.gz, .pdf, abstract, bibtex )
- [ABBDDFHJLMPWY01] Uppaal - Now, Next, and Future, Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Pedro R. D'Argenio, Alexandre David, Ansgar Fehnker, Thomas Hune, Bertrand Jeannet, Kim G. Larsen, M. Oliver Möller, Paul Pettersson, Carsten Weise, and Wang Yi. In Proceedings of Modelling and Verification of Parallel Processes (MOVEP'2k), Nantes, France, June 19 to 23, 2000. LNCS Tutorial 2067, pages 100-125, F. Cassez, C. Jard, B. Rozoy, and M. Ryan (Eds.), 2001. ( .ps.gz, .pdf, abstract, bibtex )
- [BFHLPR01] Efficient Guiding Towards Cost-Optimality in Uppaal, Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, and Judi Romijn. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01). Genova, Italy, April 2 to 6, 2001. LNCS 2031, pages 174-188, T. Margaria and W. Yi (Eds.). ( .ps.gz, .pdf, abstract, bibtex )
- [BFHLPRV01] Minimum-Cost Reachability for Priced Timed Automata, Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn, and Frits Vaandrager. In Proceedings of the 4th International Workwhop on Hybrid Systems: Computation and Control (HSCC'01). Rome, Italy, March 28 to 30, 2001. LNCS 2034, pages 147-161, Maria Domenica Di Benedetto and Alberto Sangiovanni-Vincentelli (Eds.). ( .ps.gz, .pdf, abstract, bibtex )
- [DW00] Modelling and Analysis of a Commercial Field Bus Protocol, Alexandre David and Wang Yi. In Proceedings of the 12th Euromicro Conference on Real Time Systems pages 165-172, 2000 (ps.gz, bibtex)
- [IKLLMMPT00] Model-Checking Real-Time Control Programs, Torsten K. Iversen, Kåre J. Kristoffersen, Kim G. Larsen, Morten Laursen, Rune G. Madsen, Steffen K. Mortensen, Paul Pettersson and Chris B. Thomasen. In Proceedings of the 12th Euromicro Conference on Real-Time Systems (ECRTS'2000), pages 147-155. Stockholm, Sweden, June 19 - 21, 2000. ( .ps.gz, .pdf, abstract, bibtex )
- [BHVCAV00] Distributing Timed Model Checking -- How the Search Order Matters, Gerd Behrmann, Thomas Hune, and Frits Vaandrager. In Proc. of 12th International Conference on Computer Aided Verification, CAV2000, Lecture Notes in Computer Science, Chicago, Juli 2000. Springer-Verlag. (.ps.gz, .pdf, abstract, bibtex).
- [HLP00] Guided Synthesis of Control Programs Using Uppaal,Thomas Hune, Kim G. Larsen and Paul Pettersson. Accepted for presentation at the International Workshop on Distributed Systems Verification and Validation. Taipei, Taiwan, April 10-13, 2000. ( .ps.gz, .pdf, abstract, bibtex ).
- [LPW00] On Memory-Block Traversal Problems in Model Checking Timed Systems, Fredrik Larssson, Paul Pettersson and Wang Yi. Accepted for presentation at the 6th International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Germany, March 27 - April 1, 2000. ( ps.gz, pdf, abstract, bibtex ).
- [HLS99] Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal. Klaus Havelund, Kim G. Larsen and Arne Skou. Accepted for presentation at 5th International AMAST Workshop on Real-Time and Probabilistic Systems.
- [KLPW99] Experimental Batch Plant - VHS Case Study 1 Using Timed Automata and Uppaal. Kåre J. Kristoffersen, Kim G. Larsen, Paul Pettersson and Carsten Weise. Deliverable of EPRIT-LTR Project 26270 VHS (Verification of Hybird Systems). ( .ps, .pdf, abstract, bibtex ).
- [BLPWW99] Efficient Timed Reachability Analysis Using Clock Difference Diagrams. Gerd Behrmann, Kim G. Larsen, Justin Pearson, Carsten Weise, and Wang Yi. Accepted for presentation at CAV99.
- [PET99] Modelling and Verification of Real-Time Systems Using Timed Automata:Theory and Practice, Paul Pettersson. Ph.D. Thesis, Technical Report DoCs 99/101, department of Computer Systems, Uppsala University, 19 February 1999.
- [LWYP98] Clock Difference Diagrams. Kim G. Larsen, Carsten Weise, Wang Yi and Justin Pearson. DoCS Technical Report Nr 98/99, Uppsala University, ISSN 0283-0574, August 1998. (pdf).
- [BFM98] Specification and verification of media constraints using Uppaal. H. Bowman, G. Faconti, and M. Massink. In 5th Eurographics Workshop on the Design, Specification and Verification of Interactive Systems, Eurographics Series. Springer-Verlag, August 1998.
- [BJLW98] Partial Order Reductions for Timed Systems. Johan Bengtsson, Bengt Jonsson, Johan Lilius and Wang Yi. In proceedings of the 9th International Conference on Concurrency Theory. Nice, France, September 1998. (pdf).
- [BLLPWW98] New Generation of Uppaal. Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi and Carsten Weise. In proceedings of the International Workshop on Software Tools for Technology Transfer. Aalborg, Denmark, 12 - 13 July, 1998.( ps.gz, pdf, abstract, bibtex).
- [BFKLM98] Automatic Verification of a Lip Synchronisation Algorithm using Uppaal. H. Bowman, G. Faconti, J-P. Katoen, D. Latella and M. Massink. In Proceedings of the 3rd International Workshop on Formal Methods for Industrial Critical Systems. Amsterdam, The Netherlands, 1998. Jan Friso Groote, Bas Luttik and Jos van Wamel (Eds.).
- [LPW98] Formal Design and Analysis of a Gear Controller. Magnus Lindahl, Paul Pettersson and Wang Yi. In Proceedings of the 4th International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Gulbenkian Foundation, Lisbon, Portugal, 31 March - 2 April, 1998. LNCS 1384, pages 281-297, Bernhard Steffen (Ed.).(ps.gz, pdf, abstract, bibtex).
- [ABL98] Model Checking via Reachability Testing for Timed Automata Luca Aceto, Augusto Bergueno and Kim G. Larsen. . In Proceedings of the 4th International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Gulbenkian Foundation, Lisbon , Portugal, 31 March - 2 April, 1998. LNCS 1384, pages 263-280, Bernhard Steffen (Ed.).
- [LPW97b]. Uppaal in a Nutshell. Kim G. Larsen, Paul Pettersson and Wang Yi. In Springer International Journal of Software Tools for Technology Transfer 1(1+2), 1997.( ps.gz, pdf, abstract, bibtex).
- [LP97] Formal Verification of a TDMA Protocol Start-Up Mechanism. Henrik Lテカnn and Paul Pettersson. In Proceedings of 1997 IEEE Pacific Rim International Symposium on Fault-Tolerant Systems, pages 235-242. Taipei, Taiwan, 15-16 December, 1997. (ps.gz, pdf, abstract, bibtex).
- [HSLL97] Formal Modelling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using Uppaal. Klaus Havelund, Arne Skou, Kim G. Larsen and Kristian Lund. In Proceedings of the 18th IEEE Real-Time Systems Symposium, pages 2-13. San Francisco, California, USA, 3-5 December 1997.
- [LLPW97] Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction. Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. In Proceedings of the 18th IEEE Real-Time Systems Symposium, pages 14-24. San Francisco, California, USA, 3-5 December 1997.( ps.gz, pdf, abstract, bibtex).
- [LPW97a]. Uppaal: Status & Developments. Kim G. Larsen, Paul Pettersson and Wang Yi. In Proceedings of the 9th International Conference on Computer-Aided Verification. Haifa, Israel, 22-25 June 1997. ( ps.gz, pdf, abstract, bibtex).
- [KLLPW97], A Compositional Proof of a Real-Time Mutual Exclusion Protocol. Kåre J. Kristoffersen, Francois Larroussinie, Kim G. Larsen, Paul Pettersson and Wang Yi. In Proceedings of the 7th International Joint Conference on the Theory and Practice of Software Development. Lille, France, 14-18 April, 1997.
- [DKRT97] The bounded retransmission protocol must be on time! P.R. D'Argenio, J.-P. Katoen, T.C. Ruys, and J. Tretmans. . In Proceedings of the 3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Enschede, The Netherlands, April 1997. LNCS 1217, pages 416-431.
- [JLS96] Modelling and Analysis of a Collision Avoidance Protocol using SPIN and Uppaal.Henrik Ejersbo Jensen, Kim G. Larsen, and Arne Skou. In Proceedings of the 2nd SPIN Workshop. Rutgers University, New Jersey, USA, 5 August 1996.
- [DKRT96] Modeling and Verifying a Bounded Retransmission Protocol. P.R. D'Argenio, J.-P. Katoen, T. Ruys, and J. Tretmans. In Proceedings of COST 247, International Workshop on Applied Formal Methods in System Design. Maribor, Slovenia, June, 1996. Also appeared as Technical Report CTIT 96-22, University of Twente, July 1996.
- [BGKLLPW96] Verification of an Audio Protocol with Bus Collision Using Uppaal. Johan Bengtsson, W. O. David Griffioen, Kåre J. Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. In Proceedings of the 8th International Conference on Computer-Aided Verification. New Brunswick, New Jersey, USA, 31 July 31-3 August, 1996. LNCS 1102, pages 244-256, R. Alur and T. A. Henzinger (Eds.) ( ps.gz, pdf, abstract, bibtex ).
- [BLLPW96] Uppaal in 1995. Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi. In Proceedings of Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Passau, Germany, 27-29 March, 1996. LNCS 1055, pages 431-434, T. Margaria and B. Steffen (Eds.).( ps.gz, pdf, abstract, bibtex).
- [BL96] Uppaal a Tool for Automatic Verification of Real-Time Systems. Johan Bengtsson and Fredrik Larsson. DoCS Technical Report Nr 96/67, Uppsala University, ISSN 0283-0574, January 1996. (pdf)
- [LPW95c] Compositional and Symbolic Model-Checking of Real-Time Systems. Kim G. Larsen, Paul Pettersson and Wang Yi. In Proceedings of the 16th IEEE Real-Time Systems Symposium, Pisa, Italy, 5-7 December, 1995.( ps.gz, pdf, abstract, bibtex).
- [BLLPW95] Uppaal - a Tool Suite for Automatic Verification of Real-Time Systems. Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. In Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, 22-24 October, 1995. ( ps.gz, pdf, abstract, bibtex ).
- [LPW95b] Diagnostic Model-Checking for Real-Time Systems. Kim G. Larsen, Paul Pettersson and Wang Yi. In Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, 22-24 October, 1995 ( ps, pdf, abstract, bibtex ).
- [LPW95a] Model-Checking for Real-Time Systems. Kim G. Larsen, Paul Pettersson and Wang Yi. In Proceedings of the 10th International Conference on Fundamentals of Computation Theory, Dresden, Germany, 22-25 August, 1995. LNCS 965, pages 62-88, Horst Reichel (Ed.). ( ps.gz, pdf, abstract, bibtex).
- [WPD94] Automatic Verification of Real-Time Communicating Systems by Constraint Solving. Wang Yi, Paul Pettersson and Mats Daniels. In Proceedings of the 7th International Conference on Formal Description Techniques, Berne, Switzerland, 4-7 October, 1994. ( ps.gz, pdf, abstract, bibtex).