Verifying time partitioning in the DEOS scheduling kernel

DOI10.1007/s10703-005-1490-4zbMath1083.68575OpenAlexW2040836231MaRDI QIDQ816194

John Penix, Eric Engstrom, Aaron Larson, Nicholas Weininger, Willem Visser, 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)

Related Items (3)

Combining Model Checking and Testing ⋮ Cost enforcement in the real-time specification for Java ⋮ Verifying time partitioning in the DEOS scheduling kernel

Uses Software

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

Cites Work

• Verifying time partitioning in the DEOS scheduling kernel
• Model checking JAVA programs using JAVA PathFinder
• Software is different
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Abstract interpretation and application to logic programs
• Lazy abstraction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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