UPPAAL - now, next, and future

Tobias Amnell; Gerd Behrmann; Johan Bengtsson; Pedro R. D'Argenio; Alexandre David; Ansgar Fehnker; Thomas Hune; Bertrand Jeannet; Kim G. Larsen; M. Oliver Möller; Paul Pettersson; Carsten Weise; Wang Yi

doi:10.1007/3-540-45510-8_4

UPPAAL - now, next, and future

Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Pedro R. D'Argenio, Alexandre David, Ansgar Fehnker, Thomas Hune, Bertrand Jeannet, Kim G. Larsen, M. Oliver Möller, Paul Pettersson, Carsten Weise, Wang Yi

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

Abstract

Uppaal is a tool for modeling, simulation and verification of real-time systems, developed jointly by BRICS at Aalborg University and the Department of Computer Systems at Uppsala University. The tool 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. Typical application areas include real-time controllers and communication protocols, in particular those where timing aspects are critical.

This paper reports on the currently available version and summarizes developments during the last two years. We report on new directions that extends Uppaal with cost-optimal exploration, parametric modeling, stop-watches, probablistic modeling, hierachical modeling, executable timed automata, and a hybrid automata animator. We also report on recent work to improve the efficiency of the tool. In particular, we outline Clock Difference Diagrams (CDDs), new compact representations of states, a distributed version of the tool, and application of dynamic partitioning.

Uppaal has been applied in a number of academic and industrial case studies. We describe a selection of the recent case studies.

Original language	English
Title of host publication	Modeling and Verification of Parallel Processes
Subtitle of host publication	4th Summer School, MOVEP 2000 Nantes, France, June 19-23, 2000, Revised Tutorial Lectures
Editors	Franck Cassez, Claude Jard, Brigitte Rozoy, Mark Dermot Ryan
Place of Publication	Berlin
Publisher	Springer, Springer Nature
Chapter	4
Pages	99-124
Number of pages	26
ISBN (Print)	9783540427872, 3540427872
DOIs	https://doi.org/10.1007/3-540-45510-8_4
Publication status	Published - 2001
Externally published	Yes

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2067
ISSN (Print)	0302-9743

Access to Document

10.1007/3-540-45510-8_4

Cite this

Amnell, T., Behrmann, G., Bengtsson, J., D'Argenio, P. R., David, A., Fehnker, A., Hune, T., Jeannet, B., Larsen, K. G., Möller, M. O., Pettersson, P., Weise, C., & Yi, W. (2001). UPPAAL - now, next, and future. In F. Cassez, C. Jard, B. Rozoy, & M. D. Ryan (Eds.), Modeling and Verification of Parallel Processes: 4th Summer School, MOVEP 2000 Nantes, France, June 19-23, 2000, Revised Tutorial Lectures (pp. 99-124). (Lecture Notes in Computer Science; Vol. 2067). Springer, Springer Nature. https://doi.org/10.1007/3-540-45510-8_4

Amnell, Tobias ; Behrmann, Gerd ; Bengtsson, Johan et al. / UPPAAL - now, next, and future. Modeling and Verification of Parallel Processes: 4th Summer School, MOVEP 2000 Nantes, France, June 19-23, 2000, Revised Tutorial Lectures. editor / Franck Cassez ; Claude Jard ; Brigitte Rozoy ; Mark Dermot Ryan. Berlin : Springer, Springer Nature, 2001. pp. 99-124 (Lecture Notes in Computer Science).

@inproceedings{6b8d2ebf512d4be8b99c76721c6a233d,

title = "UPPAAL - now, next, and future",

abstract = "Uppaal is a tool for modeling, simulation and verification of real-time systems, developed jointly by BRICS at Aalborg University and the Department of Computer Systems at Uppsala University. The tool 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. Typical application areas include real-time controllers and communication protocols, in particular those where timing aspects are critical.This paper reports on the currently available version and summarizes developments during the last two years. We report on new directions that extends Uppaal with cost-optimal exploration, parametric modeling, stop-watches, probablistic modeling, hierachical modeling, executable timed automata, and a hybrid automata animator. We also report on recent work to improve the efficiency of the tool. In particular, we outline Clock Difference Diagrams (CDDs), new compact representations of states, a distributed version of the tool, and application of dynamic partitioning.Uppaal has been applied in a number of academic and industrial case studies. We describe a selection of the recent case studies.",

author = "Tobias Amnell and Gerd Behrmann and Johan Bengtsson and D'Argenio, {Pedro R.} and Alexandre David and Ansgar Fehnker and Thomas Hune and Bertrand Jeannet and Larsen, {Kim G.} and M{\"o}ller, {M. Oliver} and Paul Pettersson and Carsten Weise and Wang Yi",

year = "2001",

doi = "10.1007/3-540-45510-8_4",

language = "English",

isbn = "9783540427872",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Springer Nature",

pages = "99--124",

editor = "Franck Cassez and Claude Jard and Brigitte Rozoy and Ryan, {Mark Dermot}",

booktitle = "Modeling and Verification of Parallel Processes",

address = "United States",

}

Amnell, T, Behrmann, G, Bengtsson, J, D'Argenio, PR, David, A, Fehnker, A, Hune, T, Jeannet, B, Larsen, KG, Möller, MO, Pettersson, P, Weise, C & Yi, W 2001, UPPAAL - now, next, and future. in F Cassez, C Jard, B Rozoy & MD Ryan (eds), Modeling and Verification of Parallel Processes: 4th Summer School, MOVEP 2000 Nantes, France, June 19-23, 2000, Revised Tutorial Lectures. Lecture Notes in Computer Science, vol. 2067, Springer, Springer Nature, Berlin, pp. 99-124. https://doi.org/10.1007/3-540-45510-8_4

UPPAAL - now, next, and future. / Amnell, Tobias; Behrmann, Gerd; Bengtsson, Johan et al.
Modeling and Verification of Parallel Processes: 4th Summer School, MOVEP 2000 Nantes, France, June 19-23, 2000, Revised Tutorial Lectures. ed. / Franck Cassez; Claude Jard; Brigitte Rozoy; Mark Dermot Ryan. Berlin: Springer, Springer Nature, 2001. p. 99-124 (Lecture Notes in Computer Science; Vol. 2067).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - UPPAAL - now, next, and future

AU - Amnell, Tobias

AU - Behrmann, Gerd

AU - Bengtsson, Johan

AU - D'Argenio, Pedro R.

AU - David, Alexandre

AU - Fehnker, Ansgar

AU - Hune, Thomas

AU - Jeannet, Bertrand

AU - Larsen, Kim G.

AU - Möller, M. Oliver

AU - Pettersson, Paul

AU - Weise, Carsten

AU - Yi, Wang

PY - 2001

Y1 - 2001

N2 - Uppaal is a tool for modeling, simulation and verification of real-time systems, developed jointly by BRICS at Aalborg University and the Department of Computer Systems at Uppsala University. The tool 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. Typical application areas include real-time controllers and communication protocols, in particular those where timing aspects are critical.This paper reports on the currently available version and summarizes developments during the last two years. We report on new directions that extends Uppaal with cost-optimal exploration, parametric modeling, stop-watches, probablistic modeling, hierachical modeling, executable timed automata, and a hybrid automata animator. We also report on recent work to improve the efficiency of the tool. In particular, we outline Clock Difference Diagrams (CDDs), new compact representations of states, a distributed version of the tool, and application of dynamic partitioning.Uppaal has been applied in a number of academic and industrial case studies. We describe a selection of the recent case studies.

AB - Uppaal is a tool for modeling, simulation and verification of real-time systems, developed jointly by BRICS at Aalborg University and the Department of Computer Systems at Uppsala University. The tool 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. Typical application areas include real-time controllers and communication protocols, in particular those where timing aspects are critical.This paper reports on the currently available version and summarizes developments during the last two years. We report on new directions that extends Uppaal with cost-optimal exploration, parametric modeling, stop-watches, probablistic modeling, hierachical modeling, executable timed automata, and a hybrid automata animator. We also report on recent work to improve the efficiency of the tool. In particular, we outline Clock Difference Diagrams (CDDs), new compact representations of states, a distributed version of the tool, and application of dynamic partitioning.Uppaal has been applied in a number of academic and industrial case studies. We describe a selection of the recent case studies.

U2 - 10.1007/3-540-45510-8_4

DO - 10.1007/3-540-45510-8_4

M3 - Conference proceeding contribution

SN - 9783540427872

SN - 3540427872

T3 - Lecture Notes in Computer Science

SP - 99

EP - 124

BT - Modeling and Verification of Parallel Processes

A2 - Cassez, Franck

A2 - Jard, Claude

A2 - Rozoy, Brigitte

A2 - Ryan, Mark Dermot

PB - Springer, Springer Nature

CY - Berlin

ER -

Amnell T, Behrmann G, Bengtsson J, D'Argenio PR, David A, Fehnker A et al. UPPAAL - now, next, and future. In Cassez F, Jard C, Rozoy B, Ryan MD, editors, Modeling and Verification of Parallel Processes: 4th Summer School, MOVEP 2000 Nantes, France, June 19-23, 2000, Revised Tutorial Lectures. Berlin: Springer, Springer Nature. 2001. p. 99-124. (Lecture Notes in Computer Science). doi: 10.1007/3-540-45510-8_4

UPPAAL - now, next, and future

Abstract

Publication series

Access to Document

Fingerprint

Cite this