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

DOI10.1016/J.TCS.2016.12.020MaRDI QIDQ507600zbMATH OpenOpenAlexFDO

Authors Omar Al-Bataineh, Tim French, Mark Alexander Reynolds

Publication date 6 February 2017

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

Full work available at URL https://arxiv.org/abs/1610.09795, http://api.research-repository.uwa.edu.au/files/41024229/TCS.pdf

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)

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.

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

Cites work

• scientific article; zbMATH DE number 1701758 (Why is no real title available?)
• scientific article; zbMATH DE number 1956585 (Why is no real title available?)
• scientific article; zbMATH DE number 7088727 (Why is no real title available?)
• A quadratic-time DBM-based successor algorithm for checking timed automata
• A theory of timed automata
• Checking timed Büchi automata emptiness efficiently
• Computer Aided Verification
• Efficient Detection of Zeno Runs in Timed Automata
• Finding Best and Worst Case Execution Times of Systems Using Difference-Bound Matrices
• Formal Methods for the Design of Real-Time Systems
• Formal Methods for the Design of Real-Time Systems
• Formal Modeling and Analysis of Timed Systems
• Forward analysis of updatable timed automata
• Lectures on Concurrency and Petri Nets
• Minimum and maximum delay problems in real-time systems
• Static detection of Zeno runs in UPPAAL networks based on synchronization matrices and two data-variable heuristics

Cited in

(2)

• Time separations of cyclic event rule systems with min-max timing constraints
• Accelerating worst case execution time analysis of timed automata models with cyclic behaviour

Describes a project that uses

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)