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].
- Tutorial on Uppaal. Revised and extended version of [BDL04]. This document is updated regularly (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 in Latex, by Marius Mikucionis.
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 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.
- 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.
- 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 the socketserver 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. The socketserver 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 attacks.
- 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, where code is the language code of a supported language, currently en, zh, ja, da, lt. 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 to java -Duser.language=[code] -jar <path to uppaal.jar>.
- 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. - 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
"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 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.
Published Material
Incomplete list of publications realted to Uppaal.
- [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).