Refinement of trace abstraction for real-time programs

Franck Cassez, Peter Gjøl Jensen*, Kim Guldstrand Larsen

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

4 Citations (Scopus)

Abstract

Real-time programs are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. We report on the implementation of our algorithm and we show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.

Original languageEnglish
Title of host publicationReachability Problems
Subtitle of host publication11th International Workshop, RP 2017, Proceedings
EditorsMatthew Hague, Igor Potapov
Place of PublicationCham, Switzerland
PublisherSpringer, Springer Nature
Pages42-58
Number of pages17
Volume10506
ISBN (Electronic)9783319670898
ISBN (Print)9783319670881
DOIs
Publication statusPublished - 2017
Event11th International Workshop on Reachability Problems, RP 2017 - London, United Kingdom
Duration: 7 Sep 20179 Sep 2017

Publication series

NameLecture Notes in Computer Science
Volume10506
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference11th International Workshop on Reachability Problems, RP 2017
CountryUnited Kingdom
CityLondon
Period7/09/179/09/17

Fingerprint Dive into the research topics of 'Refinement of trace abstraction for real-time programs'. Together they form a unique fingerprint.

  • Cite this

    Cassez, F., Jensen, P. G., & Guldstrand Larsen, K. (2017). Refinement of trace abstraction for real-time programs. In M. Hague, & I. Potapov (Eds.), Reachability Problems: 11th International Workshop, RP 2017, Proceedings (Vol. 10506, pp. 42-58). (Lecture Notes in Computer Science; Vol. 10506). Cham, Switzerland: Springer, Springer Nature. https://doi.org/10.1007/978-3-319-67089-8_4