Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Uppaal Model Checker
open-in-new
<p>UPPAAL is an integrated <a href="/facts/Tool/KhhEHz1I">tool</a> <a href="/facts/Software_platform/DmKwp5Bk">environment</a> for <a href="/facts/Model_checking/FwvKMlw9">modeling</a>, validation and verification of <a href="/facts/Real-time_computing/p9HxgL4L">real-time</a> systems modeled as networks of <a href="/facts/Timed_automaton/Ca89Xnbd">timed automata</a>, extended with <a href="/facts/Data_type/fcx5hgVL">data types</a> (bounded integers, arrays etc.). </p><p>It has been used in at least 17 case studies since its release in 1995, including on <a href="/facts/Lego_Mindstorms/WhKlrqE6">Lego Mindstorms</a>, for the <a href="/facts/Philips/Xp4uczGg">Philips</a> audio protocol, and in gearbox controllers for <a href="/facts/Mecel/Xc9yTa9Q">Mecel</a>. </p><p>The tool has been developed in collaboration between the Design and Analysis of Real-Time Systems group at <a href="/facts/Uppsala_University/zQbWhyqc">Uppsala University</a>, <a href="/facts/Sweden/u3qC7lyj">Sweden</a> and Basic Research in Computer Science at <a href="/facts/Aalborg_University/JKk90Y0I">Aalborg University</a>, <a href="/facts/Denmark/KVtykzsw">Denmark</a>. </p><p>There are the following extensions available: </p> <ul><li><a href="http://people.cs.aau.dk/~adavid/cora/">Cora</a> for Cost Optimal Reachability Analysis.</li> <li><a href="http://people.cs.aau.dk/~marius/tron/">Tron</a> for Testing Real-time systems ON-line (black-box conformance testing).</li> <li><a href="http://user.it.uu.se/~hessel/CoVer/">Cover</a> for COVERerage-optimal off-line test generation.</li> <li><a href="http://people.cs.aau.dk/~adavid/tiga/">Tiga</a> for TImed GAmes based controller synthesis.</li> <li><a href="http://www.it.uu.se/research/group/darts/uppaal/port/">Port</a> for component based timed systems, exploiting Partial Order Reduction Techniques.</li> <li>Pro for PRObabilistic reachability analysis. (Discontinued)</li> <li><a href="http://people.cs.aau.dk/~adavid/smc/">SMC</a> for Statistical Model Checking.</li></ul>