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.

References in zbMATH (referenced in 42 articles , 1 standard article )

Showing results 1 to 20 of 42.
Sorted by year (citations)

1 2 3 next

  1. Jaghoori, Mohammad Mahdi; de Boer, Frank; Longuet, Delphine; Chothia, Tom; Sirjani, Marjan: Compositional schedulability analysis of real-time actor-based systems (2017)
  2. Motallebi, Hassan; Azgomi, Mohammad Abdollahi: Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets (2012)
  3. Lomuscio, Alessio; Penczek, Wojciech; Solanki, Monika; Szreter, Maciej: Runtime monitoring of contract regulated web services (2011)
  4. André, Étienne; Chatain, Thomas; Fribourg, Laurent; Encrenaz, Emmanuelle: An inverse method for parametric timed automata (2009)
  5. Jaghoori, Mohammad Mahdi; de Boer, Frank S.; Chothia, Tom; Sirjani, Marjan: Schedulability of asynchronous real-time concurrent objects (2009)
  6. Kot, Martin: Modeling selected real-time database concurrency control protocols in Uppaal (2009) ioport
  7. Schlich, Bastian; Kowalewski, Stefan: Model checking C source code for embedded systems (2009) ioport
  8. Zhang, Miaomiao; Liu, Zhiming; Morisset, Charles; Ravn, Anders P.: Design and verification of fault-tolerant components (2009)
  9. Bérard, B.; Cassez, F.; Haddad, S.; Lime, D.; Roux, O.H.: When are timed automata weakly timed bisimilar to time Petri nets? (2008)
  10. Janowska, Agata; Janowski, Paweł; Wróblewski, Dobiesław: Translation of intermediate language to timed automata with discrete data (2008)
  11. Penczek, Wojciech; Szreter, Maciej: SAT-based unbounded model checking of timed automata (2008)
  12. Kwiatkowska, Marta; Norman, Gethin; Sproston, Jeremy; Wang, Fuzhi: Symbolic model checking for probabilistic timed automata (2007)
  13. Villani, Emilia; Miyagi, Paulo Eigi; Valette, Robert: Modelling and analysis of hybrid supervisory systems. A Petri net approach. (2007)
  14. Janowska, Agata; Janowski, Paweł: Slicing of timed automata with discrete data (2006)
  15. Kwiatkowska, Marta; Norman, Gethin; Parker, David; Sproston, Jeremy: Performance analysis of probabilistic timed automata using digital clocks (2006)
  16. Madl, Gabor; Abdelwahed, Sherif; Schmidt, Douglas C.: Verifying distributed real-time properties of embedded systems via graph transformations and model checking (2006)
  17. Penczek, Wojciech; Półrola, Agata: Advances in verification of time Petri nets and timed automata. A temporal logic approach. (2006)
  18. Bowman, Howard; Gomez, Rodolfo; Su, Li: A tool for the syntactic detection of Zeno-timelocks in timed automata (2005)
  19. De Wulf, Martin; Doyen, Laurent; Raskin, Jean-François: Almost ASAP semantics: from timed models to timed implementations (2005)
  20. Ernits, Juhan: Memory arbiter synthesis and verification for a radar memory interface card (2005)

1 2 3 next