Previous Presentations

Here is a small collection of previous presentations on UPPAAL that may prove useful to understand the tool and its underlying algorithms.

• PDF: Symbolic reachability and beyond (Kim, 2001, DTU).
• PDF: UPPAAL in teaching (Paul, 2003, ASTEC).
• EEF Concurrency School 2003 (Kim & Gerd)
  • Introduction
  • Regions
  • Introduction to UPPAAL
  • Verification Options
  • Efficient Verification
  • Hybrid Systems
  • Scheduling
  • Infinite Schedules
  • Logics and Preorders
  • Stopwatch Automata
  • To Store or Not To Store
• PDF: Merging DBMs efficiently (Alexandre, 2005, NWPT).
• PDF: Beyond Liveness - Efficient Parameter Synthesis for Timed Bounded Liveness (Kim, 2005, FORMATS).
• 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.

Existing courses

UPPAAL is used in courses on real-time systems or formal methods. Here are some of the existing courses.

• Formal analysis methods for real-time systems given in Uppsala in Spring 2004. Links to exercises: 1, 2, 3, and 4. Link to the project.
• Validation of embedded systems given in Aalborg in fall 2004. Modeling exercise.