swMATH ID: 1595
Software Authors: Kim G. Larsen, Wang Yi, Paul Pettersson, Alexandre David, Brian Nielsen, Arne Skou, John Håkansson, Jacob Illum Rasmussen, Pavel Krcál, Ulrik Larsen, Marius Mikucionis, Leonid Mokrushin
Description: Uppaal is an integrated tool environment for modeling, simulation and verification of real-time systems, developed jointly by Basic Research in Computer Science at Aalborg University in Denmark and the Department of Information Technology at Uppsala University in Sweden. It is appropriate for systems that can be modeled as a collection of non-deterministic processes with finite control structure and real-valued clocks, communicating through channels or shared variables [WPD94, LPW97b]. Typical application areas include real-time controllers and communication protocols in particular, those where timing aspects are critical. Since its first release in 1995, Uppaal has been applied in a number of case studies (see section Case Studies). To meet requirements arising from the case studies, the tool has been extended with various features. The current version of Uppaal, called Uppaal2k, was first released in September 1999. It is a client/server application implemented in Java and C++, and is currently available for Linux, SunOS and Windows 95/98/NT. The features of Uppaal2k include: A graphical system editor allowing graphical descriptions of systems. A graphical simulator which provides graphical visualization and recording of the possible dynamic behaviors of a system description, i.e. sequences of symbolic states of the system. It may also be used to visualize traces generated by the model-checker. Since version 3.4 the simulator can visualize a trace as a message sequence chart (MSC). A requirement specification editor that also constitutes a graphical user interface to the verifier of Uppaal2k. A model-checker for automatic verification of safety and bonded-liveness properties by reachability analysis of the symbolic state-space. Since version 3.2 it can also check liveness properties. Generation of diagnostic traces in case verification of a particular real-time system fails. The diagnostic traces may be automatically loaded and graphically visualized using the simulator. Since version 3.4 it is possible to specify that the generated trace should be the shortest or the fastest.
Homepage: http://www.it.uu.se/research/group/darts/uppaal/about.shtml
Keywords: model checking; leader election algorithms
Related Software: Uppaal; Kronos; HyTech; PRISM; SPIN; VerICS; Rabbit; TREX; CADP; TINA; Eiffel; TAXYS; IF-2.0; E-LOTOS; UPPAAL CORA; fc2tools; Chaff; Design/CPN; CPN/Tools; CUDD
Cited in: 38 Documents

Citations by Year