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 checkingqueuestimed automataschedulabilitythree-valued abstraction

Mathematics Subject Classification ID

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

Recommendations

• Compositional Abstraction in Real-Time Model Checking
• scientific article; zbMATH DE number 1949600
• 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

• scientific article; zbMATH DE number 590999 (Why is no real title available?)
• scientific article; zbMATH DE number 2080041 (Why is no real title available?)
• scientific article; zbMATH DE number 2080044 (Why is no real title available?)
• scientific article; zbMATH DE number 2080067 (Why is no real title available?)
• scientific article; zbMATH DE number 7649924 (Why is no real title available?)
• 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
• Lectures on Concurrency and Petri Nets
• Model Checking Real-Time Systems
• Sensitivity analysis for fixed-priority real-time systems
• Three-Valued Abstraction for Continuous-Time Markov Chains
• 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)