Uppaal2k swMATH ID: 1595 Software Authors: Larsen, Kim G.; Yi, Wang; Pettersson, Paul; David, Alexandre; Nielsen, Brian; Skou, Arne; Håkansson, John; Rasmussen, Jacob Illum; Krcál, Pavel; Larsen, Ulrik; Mikucionis, Marius; Mokrushin, Leonid 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; TINA; CADP; Eiffel; TAXYS; IF-2.0; E-LOTOS; fc2tools; CPN/Tools; Chaff; Design/CPN; UPPAAL CORA; CUDD Cited in: 38 Documents Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. Zbl 1053.68580Simons, David P. L.; Stoelinga, Mariëlle I. A. 2001 all top 5 Cited by 70 Authors 5 Wang, Farn 4 Kwiatkowska, Marta Z. 4 Norman, Gethin 4 Romijn, Judi 4 Sproston, Jeremy 3 Penczek, Wojciech 3 Shankland, Carron 3 Stoelinga, Mariëlle 2 Chothia, Tom 2 de Boer, Frank S. 2 Hwang, Geng-Dian 2 Jaghoori, Mohammad Mahdi 2 Janowska, Agata 2 Janowski, Paweł 2 Maharaj, Savi 2 Sirjani, Marjan 2 Szreter, Maciej 2 Yu, Fang 1 Abdelwahed, Sherif 1 André, Étienne 1 Azgomi, Mohammad Abdollahi 1 Bérard, Béatrice 1 Biere, Armin 1 Bowman, Howard 1 Cardell-Oliver, Rachel 1 Cassez, Franck 1 Chatain, Thomas 1 D’Argenio, Pedro Rubén 1 De Wulf, Martin 1 Doyen, Laurent 1 Encrenaz, Emmanuelle 1 Ernits, Juhan 1 Fidge, Colin J. 1 Fribourg, Laurent 1 Gerdsmeier, T. 1 Gomez, Rodolfo 1 Haddad, Serge 1 Huang, Geng-Dian 1 Hune, Thomas 1 Jeannet, Bertrand 1 Jensen, Henrik Ejersbo 1 Larsen, Kim Guldstrand 1 Lime, Didier 1 Liu, Zhiming 1 Lomuscio, Alessio 1 Longuet, Delphine 1 Madl, Gabor 1 Matoušek, Petr 1 Miyagi, Paulo Eigi 1 Morisset, Charles 1 Motallebi, Hassan 1 Parker, David J. 1 Półrola, Agata 1 Raskin, Jean-François 1 Ravn, Anders P. 1 Roux, Olivier H. 1 Schmidt, Douglas C. 1 Schuppan, Viktor 1 Seidelin Hune, Thomas 1 Simons, David P. L. 1 Smrčka, Aleš 1 Solanki, Monika 1 Su, Li 1 Vaandrager, Frits W. 1 Valette, Robert 1 Villani, Emilia 1 Vojnar, Tomáš 1 Wang, Fuzhi 1 Wróblewski, Dobiesław 1 Zhang, Miaomiao all top 5 Cited in 13 Serials 7 Formal Aspects of Computing 4 Fundamenta Informaticae 2 Theoretical Computer Science 2 Formal Methods in System Design 2 The Journal of Logic and Algebraic Programming 1 Acta Informatica 1 Information and Computation 1 Real-Time Systems 1 International Journal of Foundations of Computer Science 1 Nordic Journal of Computing 1 Journal of Universal Computer Science 1 Studies in Computational Intelligence 1 Advances in Industrial Control Cited in 5 Fields 37 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) 1 Operations research, mathematical programming (90-XX) 1 Systems theory; control (93-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year