Spotlight abstraction in model checking real-time task schedulability

DOI10.1007/978-3-030-84629-9_4zbMATH Open1490.68135OpenAlexW3193861647MaRDI QIDQ832017FDOQ832017

Madoda Nxumalo, Stefan Gruner, Nils Timm

Publication date: 24 March 2022

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

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

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)

Cites Work

• A theory of timed automata
• What's decidable about hybrid automata?
• Three-Valued Abstraction for Continuous-Time Markov Chains
• Lectures on Concurrency and Petri Nets
• Title not available (Why is that?)
• Sensitivity analysis for fixed-priority real-time systems
• Better abstractions for timed automata
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Model Checking Real-Time Systems
• Title not available (Why is that?)
• Abstraction refinement algorithms for timed automata

Uses Software

• IMITATOR
• TIMES

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)