Proving fairness and implementation correctness of a microkernel scheduler

DOI10.1007/S10817-009-9119-8MaRDI QIDQ835766zbMATH OpenOpenAlexFDO

Authors Matthias Daum, Jan Dörrenbächer, Burkhart Wolff

Publication date 31 August 2009

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-009-9119-8

zbMATH Keywords

formal verificationinteractive theorem provingIsabelle/HOLmicrokernel

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Recommendations

• Theorem Proving in Higher Order Logics
• Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
• From a proven correct microkernel to trustworthy large systems
• scientific article; zbMATH DE number 3901999
• Modular verification of preemptive OS kernels

Cites work

• A formulation of the simple theory of types
• An introduction to mathematical logic and type theory: To truth through proof.
• Balancing the load. Leveraging a semantics stack for systems verification
• Formal Pervasive Verification of a Paging Mechanism
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• Isabelle/HOL. A proof assistant for higher-order logic
• Logic for Programming, Artificial Intelligence, and Reasoning
• Operating system verification---an overview
• Realistic Worst-Case Execution Time Analysis in the Context of Pervasive System Verification
• Secure Microkernels, State Monads and Scalable Refinement
• Using XCAP to Certify Realistic Systems Code: Machine Context Management
• Verifying a signature architecture: a comparative case study

Cited in

(6)

• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• Balancing the load. Leveraging a semantics stack for systems verification
• An intuitive formal proof for deadline driven scheduler
• Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
• A corrigendum to: ``Sticky-ERfair: a task-processor affinity aware proportional fair scheduler
• Priority inheritance protocol proved correct

Describes a project that uses

Uses Software

• Boogie
• ETPS
• Caduceus
• Why3
• KRAKATOA
• Isabelle/HOL
• veriSoft
• Isabelle
• HOL-Boogie
• ACL2

This page was built for publication: Proving fairness and implementation correctness of a microkernel scheduler

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