Finding minimum and maximum termination time of timed automata models with cyclic behaviour

DOI10.1016/J.TCS.2016.12.020zbMATH Open1357.68109arXiv1610.09795OpenAlexW2548654831MaRDI QIDQ507600FDOQ507600

Mark Alexander Reynolds, Omar Al-Bataineh, Tim French

Publication date: 6 February 2017

Published in: Theoretical Computer Science (Search for Journal in Brave)

Abstract: The paper presents a novel algorithm for computing best and worst case execution times (BCET/WCET) of timed automata models with cyclic behaviour. The algorithms can work on any arbitrary diagonal-free TA and can handle more cases than previously existing algorithms for BCET/WCET computations, as it can handle cycles in TA and decide whether they lead to an infinite WCET. We show soundness of the proposed algorithm and study its complexity. To our knowledge, this is the first model checking algorithm that addresses comprehensively the BCET/WCET problem of systems with cyclic behaviour. Behrmann et al. provide an algorithm for computing the minimum cost/time of reaching a goal state in priced timed automata (PTA). The algorithm has been implemented in the well-known model checking tool UPPAAL to compute the minimum time for termination of an automaton. However, we show that in certain circumstances, when infinite cycles exist, the algorithm implemented in UPPAAL may not terminate, and we provide examples which UPPAAL fails to verify.

Full work available at URL: https://arxiv.org/abs/1610.09795

Recommendations

• Accelerating worst case execution time analysis of timed automata models with cyclic behaviour
• scientific article; zbMATH DE number 1794367
• Finding Best and Worst Case Execution Times of Systems Using Difference-Bound Matrices
• scientific article; zbMATH DE number 1962849
• scientific article; zbMATH DE number 1701758

zbMATH Keywords

model checkingworst-case execution timetimed automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Formal Methods for the Design of Real-Time Systems
• A theory of timed automata
• Formal Methods for the Design of Real-Time Systems
• Lectures on Concurrency and Petri Nets
• Checking timed Büchi automata emptiness efficiently
• A quadratic-time DBM-based successor algorithm for checking timed automata
• Forward analysis of updatable timed automata
• Title not available (Why is that?)
• Title not available (Why is that?)
• Minimum and maximum delay problems in real-time systems
• Title not available (Why is that?)
• Efficient Detection of Zeno Runs in Timed Automata
• Formal Modeling and Analysis of Timed Systems
• Static Detection of Zeno Runs in UPPAAL Networks Based on Synchronization Matrices and Two Data-Variable Heuristics
• Computer Aided Verification
• Finding Best and Worst Case Execution Times of Systems Using Difference-Bound Matrices

Cited In (1)

• Time separations of cyclic event rule systems with min-max timing constraints

Uses Software

• Kronos
• Uppaal
• opaal
• Algorithm 97

This page was built for publication: Finding minimum and maximum termination time of timed automata models with cyclic behaviour

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q507600)