Spotlight abstraction in model checking real-time task schedulability

DOI10.1007/978-3-030-84629-9_4MaRDI QIDQ832017zbMATH OpenOpenAlexFDO

Authors Madoda Nxumalo, Nils Timm, Stefan Gruner

Publication date 24 March 2022

Full work available at URL https://doi.org/10.1007/978-3-030-84629-9_4

zbMATH Keywords

model checkingqueuesschedulabilitythree-valued abstractiontimed automata

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Compositional Abstraction in Real-Time Model Checking
• An abstract model for scheduling real-time programs
• Model-checking in dense real-time
• Model-checking for real-time systems
• On Expressiveness and Complexity in Real-Time Model Checking
• Model Checking Real-Time Systems
• An abstraction technique for real-time verification
• Conformance checking of real-time models. Symbolic execution vs. bounded model checking

Cites work

• 2-valued and 3-valued abstraction-refinement in model checking
• A theory of timed automata
• Abstraction refinement algorithms for timed automata
• Better abstractions for timed automata
• scientific article; zbMATH DE number 590999 (Why is no real title available?)
• Lectures on Concurrency and Petri Nets
• Model Checking Real-Time Systems
• Preemptive job-shop scheduling using stopwatch automata
• Revisiting local time semantics for networks of timed automata
• Sensitivity analysis for fixed-priority real-time systems
• Three-Valued Abstraction for Continuous-Time Markov Chains
• Timed automata with asynchronous processes: Schedulability and decidability
• TIMES -- a tool for modelling and implementation of embedded systems
• What's decidable about hybrid automata?

Describes a project that uses

Uses Software

• TIMES
• IMITATOR

This page was built for publication: Spotlight abstraction in model checking real-time task schedulability

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