Uppaal Model Checker

{{Short description|Integrated tool environment}}

{{Infobox software

| name = UPPAAL

| logo =

| screenshot =

| caption =

| developer = Uppsala University
Aalborg University

| released = {{Start date|1995}}

| latest release version = 5.0.0

| latest release date = {{release date and age|2023|07|14}}

| latest preview version = 5.1.0-beta3

| latest preview date = {{release date and age|2023|10|23}}

| programming_language = C++ and GUI in Java

| operating system = Linux
Mac OS X
Microsoft Windows

| platform =

| genre = Model checking

| language = English Danish Japanese Chinese Lithuanian

| license = Commercial Licenses
Academic Licenses

| website = http://www.uppaal.org/ http://www.uppaal.com/

}}

UPPAAL is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays etc.).

It has been used in at least 17 case studies since its release in 1995, including on Lego Mindstorms, for the Philips audio protocol, and in gearbox controllers for Mecel.{{cite web|url=http://www.it.uu.se/research/group/darts/uppaal/examples.shtml|title=Case Studies}}

The tool has been developed in collaboration between the Design and Analysis of Real-Time Systems group at Uppsala University, Sweden and Basic Research in Computer Science at Aalborg University, Denmark.

There are the following extensions available:

• [http://people.cs.aau.dk/~adavid/cora/ Cora] for Cost Optimal Reachability Analysis.
• [http://people.cs.aau.dk/~marius/tron/ Tron] for Testing Real-time systems ON-line (black-box conformance testing).
• [http://user.it.uu.se/~hessel/CoVer/ Cover] for COVERerage-optimal off-line test generation.
• [http://people.cs.aau.dk/~adavid/tiga/ Tiga] for TImed GAmes based controller synthesis.
• [http://www.it.uu.se/research/group/darts/uppaal/port/ Port] for component based timed systems, exploiting Partial Order Reduction Techniques.
• Pro for PRObabilistic reachability analysis. (Discontinued)
• [http://people.cs.aau.dk/~adavid/smc/ SMC] for Statistical Model Checking.