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

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

7 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationNASA Formal Methods
EditorsJulia M. Badger, Kristin Yvonne Rozier
Number of pages6
Volume8430
PublisherSpringer Publishing Company
Publication date2014
Pages307-312
ISBN (Print)978-3-319-06199-3
ISBN (Electronic)978-3-319-06200-6
DOIs
Publication statusPublished - 2014
EventNASA Formal Methods - Houston, TX, United States
Duration: 29 Apr 20141 May 2014

Conference

ConferenceNASA Formal Methods
CountryUnited States
CityHouston, TX
Period29/04/201401/05/2014
SeriesLecture Notes in Computer Science
ISSN0302-9743

Cite this

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. In J. M. Badger, & K. Y. Rozier (Eds.), NASA Formal Methods (Vol. 8430, pp. 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. editor / Julia M. Badger ; Kristin Yvonne Rozier. Vol. 8430 Springer Publishing Company, 2014. pp. 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",
series = "Lecture Notes in Computer Science",
publisher = "Springer Publishing Company",
pages = "307--312",
editor = "Badger, {Julia M. } and Rozier, {Kristin Yvonne}",
booktitle = "NASA Formal Methods",
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. in JM Badger & KY Rozier (eds), NASA Formal Methods. vol. 8430, Springer Publishing Company, Lecture Notes in Computer Science, pp. 307-312, NASA Formal Methods, Houston, TX, United States, 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. ed. / Julia M. Badger; Kristin Yvonne Rozier. Vol. 8430 Springer Publishing Company, 2014. p. 307-312 (Lecture Notes in Computer Science).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-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

T3 - Lecture Notes in Computer Science

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. In Badger JM, Rozier KY, editors, NASA Formal Methods. Vol. 8430. Springer Publishing Company. 2014. p. 307-312. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-06200-6_26