Memory Efficient Data Structures for Explicit Verification of Timed Systems

Jakob Haahr Taankvist, Jiri Srba, Kim Guldstrand Larsen, Mathias Grund Sørensen, Peter Gjøl Jensen

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

7 Citationer (Scopus)

Resumé

Timed analysis of real-time systems can be performed using continuous (symbolic) or discrete (explicit) techniques. The explicit state-space exploration can be considerably faster for models with moderately small constants, however, at the expense of high memory consumption. In the setting of timed-arc Petri nets, we explore new data structures for lowering the used memory: PTries for efficient storing of configurations and time darts for semi-symbolic description of the state-space. Both methods are implemented as a part of the tool TAPAAL and the experiments document at least one order of magnitude of memory savings while preserving comparable verification times.
OriginalsprogEngelsk
TitelNASA Formal Methods
RedaktørerJulia M. Badger, Kristin Yvonne Rozier
Antal sider6
Vol/bind8430
ForlagSpringer Publishing Company
Publikationsdato2014
Sider307-312
ISBN (Trykt)978-3-319-06199-3
ISBN (Elektronisk)978-3-319-06200-6
DOI
StatusUdgivet - 2014
BegivenhedNASA Formal Methods - Houston, TX, USA
Varighed: 29 apr. 20141 maj 2014

Konference

KonferenceNASA Formal Methods
LandUSA
ByHouston, TX
Periode29/04/201401/05/2014
NavnLecture Notes in Computer Science
ISSN0302-9743

Citer dette

Taankvist, J. H., Srba, J., Larsen, K. G., Sørensen, M. G., & Jensen, P. G. (2014). Memory Efficient Data Structures for Explicit Verification of Timed Systems. I J. M. Badger, & K. Y. Rozier (red.), NASA Formal Methods (Bind 8430, s. 307-312). Springer Publishing Company. Lecture Notes in Computer Science https://doi.org/10.1007/978-3-319-06200-6_26
Taankvist, Jakob Haahr ; Srba, Jiri ; Larsen, Kim Guldstrand ; Sørensen, Mathias Grund ; Jensen, Peter Gjøl. / Memory Efficient Data Structures for Explicit Verification of Timed Systems. NASA Formal Methods. red. / Julia M. Badger ; Kristin Yvonne Rozier. Bind 8430 Springer Publishing Company, 2014. s. 307-312 (Lecture Notes in Computer Science).
@inproceedings{b4d6ea811f5a43a199a4168e7058d4da,
title = "Memory Efficient Data Structures for Explicit Verification of Timed Systems",
abstract = "Timed analysis of real-time systems can be performed using continuous (symbolic) or discrete (explicit) techniques. The explicit state-space exploration can be considerably faster for models with moderately small constants, however, at the expense of high memory consumption. In the setting of timed-arc Petri nets, we explore new data structures for lowering the used memory: PTries for efficient storing of configurations and time darts for semi-symbolic description of the state-space. Both methods are implemented as a part of the tool TAPAAL and the experiments document at least one order of magnitude of memory savings while preserving comparable verification times.",
author = "Taankvist, {Jakob Haahr} and Jiri Srba and Larsen, {Kim Guldstrand} and S{\o}rensen, {Mathias Grund} and Jensen, {Peter Gj{\o}l}",
year = "2014",
doi = "10.1007/978-3-319-06200-6_26",
language = "English",
isbn = "978-3-319-06199-3",
volume = "8430",
pages = "307--312",
editor = "Badger, {Julia M. } and Rozier, {Kristin Yvonne}",
booktitle = "NASA Formal Methods",
publisher = "Springer Publishing Company",
address = "United States",

}

Taankvist, JH, Srba, J, Larsen, KG, Sørensen, MG & Jensen, PG 2014, Memory Efficient Data Structures for Explicit Verification of Timed Systems. i JM Badger & KY Rozier (red), NASA Formal Methods. bind 8430, Springer Publishing Company, Lecture Notes in Computer Science, s. 307-312, NASA Formal Methods, Houston, TX, USA, 29/04/2014. https://doi.org/10.1007/978-3-319-06200-6_26

Memory Efficient Data Structures for Explicit Verification of Timed Systems. / Taankvist, Jakob Haahr; Srba, Jiri; Larsen, Kim Guldstrand; Sørensen, Mathias Grund; Jensen, Peter Gjøl.

NASA Formal Methods. red. / Julia M. Badger; Kristin Yvonne Rozier. Bind 8430 Springer Publishing Company, 2014. s. 307-312 (Lecture Notes in Computer Science).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

TY - GEN

T1 - Memory Efficient Data Structures for Explicit Verification of Timed Systems

AU - Taankvist, Jakob Haahr

AU - Srba, Jiri

AU - Larsen, Kim Guldstrand

AU - Sørensen, Mathias Grund

AU - Jensen, Peter Gjøl

PY - 2014

Y1 - 2014

N2 - Timed analysis of real-time systems can be performed using continuous (symbolic) or discrete (explicit) techniques. The explicit state-space exploration can be considerably faster for models with moderately small constants, however, at the expense of high memory consumption. In the setting of timed-arc Petri nets, we explore new data structures for lowering the used memory: PTries for efficient storing of configurations and time darts for semi-symbolic description of the state-space. Both methods are implemented as a part of the tool TAPAAL and the experiments document at least one order of magnitude of memory savings while preserving comparable verification times.

AB - Timed analysis of real-time systems can be performed using continuous (symbolic) or discrete (explicit) techniques. The explicit state-space exploration can be considerably faster for models with moderately small constants, however, at the expense of high memory consumption. In the setting of timed-arc Petri nets, we explore new data structures for lowering the used memory: PTries for efficient storing of configurations and time darts for semi-symbolic description of the state-space. Both methods are implemented as a part of the tool TAPAAL and the experiments document at least one order of magnitude of memory savings while preserving comparable verification times.

U2 - 10.1007/978-3-319-06200-6_26

DO - 10.1007/978-3-319-06200-6_26

M3 - Article in proceeding

SN - 978-3-319-06199-3

VL - 8430

SP - 307

EP - 312

BT - NASA Formal Methods

A2 - Badger, Julia M.

A2 - Rozier, Kristin Yvonne

PB - Springer Publishing Company

ER -

Taankvist JH, Srba J, Larsen KG, Sørensen MG, Jensen PG. Memory Efficient Data Structures for Explicit Verification of Timed Systems. I Badger JM, Rozier KY, red., NASA Formal Methods. Bind 8430. Springer Publishing Company. 2014. s. 307-312. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-06200-6_26