Dynamic Extrapolation in Extended Timed Automata

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

3 Downloads (Pure)

Abstract

Abstractions, such as extrapolation, ensure the termination of timed automata model checking. However, such methods are normally only defined for classical timed automata, whereas modern tools like Uppaal take as input timed automata extended with discrete data and C-like language constructs (XTA) making classical extrapolation excessively over-approximating if even applicable. In this paper, we propose a new dynamic extrapolation technique for XTAs that utilizes information from the immediate state of the search to find more precise extrapolation values. We determine which code snippets are relevant to obtain the extrapolation values ahead of verification using static analysis and then execute these dynamically during verification. We implement our novel extrapolation technique in Uppaal and find that it reduces the zone graph sizes by 34.7% overall compared to a classic location-clock-based extrapolation. The best case is an 82.7% reduction and the worst case is a surprising 8.2% increase.

Original languageEnglish
Title of host publicationFormal Methods and Software Engineering : 24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, QLD, Australia, November 21–24, 2023, Proceedings
EditorsYi Li, Sofiène Tahar
Number of pages17
PublisherSpringer
Publication date9 Nov 2023
Pages83-99
ISBN (Print)978-981-99-7583-9
ISBN (Electronic)978-981-99-7584-6
DOIs
Publication statusPublished - 9 Nov 2023
Event24th International Conference on Formal Engineering Methods - Brisbane, Australia
Duration: 22 Nov 202324 Nov 2023
Conference number: 24
https://formal-analysis.com/icfem/2023/

Conference

Conference24th International Conference on Formal Engineering Methods
Number24
Country/TerritoryAustralia
CityBrisbane
Period22/11/202324/11/2023
Internet address
SeriesLecture Notes in Computer Science
Volume14308
ISSN0302-9743

Keywords

  • Extended timed automata
  • Extrapolation
  • Graphs
  • Program analysis

Fingerprint

Dive into the research topics of 'Dynamic Extrapolation in Extended Timed Automata'. Together they form a unique fingerprint.

Cite this