UPPAAL implementation secrets

Gerd Behrmann; Johan Bengtsson; Alexandre David; Kim G. Larsen; Paul Pettersson; Wang Yi

doi:10.1007/3-540-45739-9_1

UPPAAL implementation secrets

Gerd Behrmann
, Johan Bengtsson
, Alexandre David
, Kim G. Larsen
, Paul Pettersson
, Wang Yi

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

52 Scopus citations

Abstract

In this paper we present the continuous and on-going development of datastructures and algorithms underlying the verification engine of the tool Uppaal. In particular, we review the datastructures of Difference Bounded Matrices, Minimal Constraint Representation and Clock Difference Diagrams used in symbolic state-space representation and -analysis for real-time systems. In addition we report on distributed versions of the tool, and outline the design and experimental results for new internal datastructures to be used in the next generation of Uppaal. Finally, we mention work on complementing methods involving acceleration, abstraction and compositionality.

Original language	English
Title of host publication	Formal Techniques in Real-Time and Fault-Tolerant Systems - 7th International Symposium, FTRTFT 2002 Co-sponsored by IFIP WG 2.2, Proceedings
Editors	Werner Damm, Ernst-Rudiger Olderog
Publisher	Springer Verlag
Pages	3-22
Number of pages	20
ISBN (Print)	9783540441656
DOIs	https://doi.org/10.1007/3-540-45739-9_1
State	Published - 2002
Externally published	Yes
Event	7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002 - Oldenburg, Germany Duration: 9 Sep 2002 → 12 Sep 2002

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2469
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002
Country/Territory	Germany
City	Oldenburg
Period	9/09/02 → 12/09/02

Access to Document

10.1007/3-540-45739-9_1

Cite this

Behrmann, G., Bengtsson, J., David, A., Larsen, K. G., Pettersson, P., & Yi, W. (2002). UPPAAL implementation secrets. In W. Damm, & E.-R. Olderog (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems - 7th International Symposium, FTRTFT 2002 Co-sponsored by IFIP WG 2.2, Proceedings (pp. 3-22). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2469). Springer Verlag. https://doi.org/10.1007/3-540-45739-9_1

Behrmann, Gerd ; Bengtsson, Johan ; David, Alexandre et al. / UPPAAL implementation secrets. Formal Techniques in Real-Time and Fault-Tolerant Systems - 7th International Symposium, FTRTFT 2002 Co-sponsored by IFIP WG 2.2, Proceedings. editor / Werner Damm ; Ernst-Rudiger Olderog. Springer Verlag, 2002. pp. 3-22 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{081fe42cfc294bb38f0ff2c7f80ee77d,

title = "UPPAAL implementation secrets",

abstract = "In this paper we present the continuous and on-going development of datastructures and algorithms underlying the verification engine of the tool Uppaal. In particular, we review the datastructures of Difference Bounded Matrices, Minimal Constraint Representation and Clock Difference Diagrams used in symbolic state-space representation and -analysis for real-time systems. In addition we report on distributed versions of the tool, and outline the design and experimental results for new internal datastructures to be used in the next generation of Uppaal. Finally, we mention work on complementing methods involving acceleration, abstraction and compositionality.",

author = "Gerd Behrmann and Johan Bengtsson and Alexandre David and Larsen, \{Kim G.\} and Paul Pettersson and Wang Yi",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2002.; 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002 ; Conference date: 09-09-2002 Through 12-09-2002",

year = "2002",

doi = "10.1007/3-540-45739-9\_1",

language = "英语",

isbn = "9783540441656",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "3--22",

editor = "Werner Damm and Ernst-Rudiger Olderog",

booktitle = "Formal Techniques in Real-Time and Fault-Tolerant Systems - 7th International Symposium, FTRTFT 2002 Co-sponsored by IFIP WG 2.2, Proceedings",

address = "德国",

}

Behrmann, G, Bengtsson, J, David, A, Larsen, KG, Pettersson, P & Yi, W 2002, UPPAAL implementation secrets. in W Damm & E-R Olderog (eds), Formal Techniques in Real-Time and Fault-Tolerant Systems - 7th International Symposium, FTRTFT 2002 Co-sponsored by IFIP WG 2.2, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2469, Springer Verlag, pp. 3-22, 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002, Oldenburg, Germany, 9/09/02. https://doi.org/10.1007/3-540-45739-9_1

UPPAAL implementation secrets. / Behrmann, Gerd; Bengtsson, Johan; David, Alexandre et al.
Formal Techniques in Real-Time and Fault-Tolerant Systems - 7th International Symposium, FTRTFT 2002 Co-sponsored by IFIP WG 2.2, Proceedings. ed. / Werner Damm; Ernst-Rudiger Olderog. Springer Verlag, 2002. p. 3-22 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2469).

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

TY - GEN

T1 - UPPAAL implementation secrets

AU - Behrmann, Gerd

AU - Bengtsson, Johan

AU - David, Alexandre

AU - Larsen, Kim G.

AU - Pettersson, Paul

AU - Yi, Wang

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 2002.

PY - 2002

Y1 - 2002

N2 - In this paper we present the continuous and on-going development of datastructures and algorithms underlying the verification engine of the tool Uppaal. In particular, we review the datastructures of Difference Bounded Matrices, Minimal Constraint Representation and Clock Difference Diagrams used in symbolic state-space representation and -analysis for real-time systems. In addition we report on distributed versions of the tool, and outline the design and experimental results for new internal datastructures to be used in the next generation of Uppaal. Finally, we mention work on complementing methods involving acceleration, abstraction and compositionality.

AB - In this paper we present the continuous and on-going development of datastructures and algorithms underlying the verification engine of the tool Uppaal. In particular, we review the datastructures of Difference Bounded Matrices, Minimal Constraint Representation and Clock Difference Diagrams used in symbolic state-space representation and -analysis for real-time systems. In addition we report on distributed versions of the tool, and outline the design and experimental results for new internal datastructures to be used in the next generation of Uppaal. Finally, we mention work on complementing methods involving acceleration, abstraction and compositionality.

UR - https://www.scopus.com/pages/publications/84974695996

U2 - 10.1007/3-540-45739-9_1

DO - 10.1007/3-540-45739-9_1

M3 - 会议稿件

AN - SCOPUS:84974695996

SN - 9783540441656

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 3

EP - 22

BT - Formal Techniques in Real-Time and Fault-Tolerant Systems - 7th International Symposium, FTRTFT 2002 Co-sponsored by IFIP WG 2.2, Proceedings

A2 - Damm, Werner

A2 - Olderog, Ernst-Rudiger

PB - Springer Verlag

T2 - 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2002

Y2 - 9 September 2002 through 12 September 2002

ER -

Behrmann G, Bengtsson J, David A, Larsen KG, Pettersson P, Yi W. UPPAAL implementation secrets. In Damm W, Olderog ER, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems - 7th International Symposium, FTRTFT 2002 Co-sponsored by IFIP WG 2.2, Proceedings. Springer Verlag. 2002. p. 3-22. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-45739-9_1

UPPAAL implementation secrets

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this