Verifying time partitioning in the DEOS scheduling kernel

DOI10.1007/S10703-005-1490-4MaRDI QIDQ816194zbMATH OpenOpenAlexFDO

Authors John Penix, Willem Visser, Eric Engstrom, Aaron Larson, Nicholas Weininger, Seung Joon Park, Corina S. Păsăreanu

Publication date 20 February 2006

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-005-1490-4

zbMATH Keywords

verificationspinpredicate abstractiontime partitioningprogram model checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification of schedulability for real-time programs
• Implementation and evaluation of global and partitioned scheduling in a real-time OS
• Verification, refinement and scheduling of real-time programs
• scientific article; zbMATH DE number 1670505
• Schedulability analysis for strictly periodic tasks in RTOS
• Timing analysis of compound scheduling policies: application to posix1003.1B
• Dynamic scheduling and fault-tolerance: Specification and verification
• Robust partitioned scheduling for real-time multiprocessor systems
• scientific article; zbMATH DE number 2080042

Cites work

• scientific article; zbMATH DE number 1670553 (Why is no real title available?)
• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1670556 (Why is no real title available?)
• scientific article; zbMATH DE number 1670562 (Why is no real title available?)
• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 1701765 (Why is no real title available?)
• scientific article; zbMATH DE number 3833669 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 108577 (Why is no real title available?)
• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• scientific article; zbMATH DE number 1956607 (Why is no real title available?)
• scientific article; zbMATH DE number 2080047 (Why is no real title available?)
• scientific article; zbMATH DE number 2087636 (Why is no real title available?)
• scientific article; zbMATH DE number 1903358 (Why is no real title available?)
• scientific article; zbMATH DE number 2102703 (Why is no real title available?)
• scientific article; zbMATH DE number 2102725 (Why is no real title available?)
• Abstract interpretation and application to logic programs
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Lazy abstraction
• Model checking JAVA programs using JAVA PathFinder
• Software is different
• Verifying time partitioning in the DEOS scheduling kernel

Cited in

(4)

• Cost enforcement in the real-time specification for Java
• Combining model checking and testing
• scientific article; zbMATH DE number 2017347 (Why is no real title available?)
• Verifying time partitioning in the DEOS scheduling kernel

Describes a project that uses

Uses Software

• dSPIN
• Bebop
• CESAR
• Bandera
• Java PathFinder
• Bogor
• SPIN
• veriSoft

This page was built for publication: Verifying time partitioning in the DEOS scheduling kernel

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