Task automata: Schedulability, decidability and undecidability

DOI10.1016/j.ic.2007.01.009zbMath1121.68062OpenAlexW2036081705MaRDI QIDQ2643078

Pavel Krcal, Paul Pettersson, Elena Fersman, Wang Yi

Publication date: 23 August 2007

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2007.01.009

zbMATH Keywords

timed automataschedulability analysisreal time systemsmodeling and verification

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (22)

Schedulability of asynchronous real-time concurrent objects ⋮ A process algebraic approach to the schedulability analysis and workload abstraction of hierarchical real-time systems ⋮ A survey of timed automata for the development of real-time systems ⋮ Combinatorial abstraction refinement for feasibility analysis of static priorities ⋮ A study on shuffle, stopwatches and independently evolving clocks ⋮ Controller synthesis for dynamic hierarchical real-time plants using timed automata ⋮ Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets ⋮ Interrupt timed automata: verification and expressiveness ⋮ Integrating deployment architectures and resource consumption in timed object-oriented models ⋮ Computing periodic request functions to speed-up the analysis of non-cyclic task models ⋮ Graph-based models for real-time workload: a survey ⋮ MODELING AND ANALYSIS OF REAL-TIME SYSTEMS WITH MUTEX COMPONENTS ⋮ Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm ⋮ Compositional schedulability analysis of real-time actor-based systems ⋮ Decomposition of timed automata for solving scheduling problems ⋮ Validating Timed Models of Deployment Components with Parametric Concurrency ⋮ PADS: an approach to modeling resource demand and supply for the formal analysis of hierarchical scheduling ⋮ A comparison of schedulability analysis methods using state and digraph models for the schedulability analysis of synchronous FSMs ⋮ Testing Concurrent Objects with Application-Specific Schedulers ⋮ Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques ⋮ Zone-based verification of timed automata: extrapolations, simulations and what next? ⋮ Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints*

Uses Software

• TIMES

Cites Work

• The algorithmic analysis of hybrid systems
• What's decidable about hybrid automata?
• A theory of timed automata
• Time-abstracted bisimulation: Implicit specifications and decidability
• Schedulability analysis of fixed-priority systems using timed automata
• Tools and Algorithms for the Construction and Analysis of Systems
• Lectures on Concurrency and Petri Nets
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Task automata: Schedulability, decidability and undecidability