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 contributionpeer-review

7 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 Sept 20179 Sept 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
Country/TerritoryUnited 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