Refinement High-Level /stem Call Abstract sy Primitive U St Applications LOW-Level Concrete Kernel ImpL
High-Level Abstract Primitive Applications Low-Level Concrete Kernel Impl. Refinement
Contextual refinement For all applications High-Level /stem Call Abstract sy Primitive U St LOW-Level Concrete Kernel ImpL
Low-Level Concrete Kernel Impl. Contextual Refinement … For all applications High-Level Abstract Primitive
Contextual refinement as OS Correctness O Ectxt s iff V A. ObsBeh (A[)c ObsBeh (A[sT The set of observable behaviors A: Application O: OS Concrete Impl. S: Abstract Prim
Contextual Refinement as OS Correctness The set of observable behaviors A：Application O：OS Concrete Impl. S：Abstract Prim. O ctxt S iff A. ObsBeh(A[O]) ObsBeh(A[S])
Outline OS Correctness Verification framework Program logic for refinement and multi-level interrupts Verifying uC/OS
Outline • OS Correctness • Verification Framework – Program logic for refinement and multi-level interrupts • Verifying μC/OS-II
OS Correctness Applications High-Level Abstract machine C+ Abstract primitives Low-Level Abstract Machine High-Level Low-Level Concrete C+Assembly Abstract Primitives Implementations
OS Correctness High-Level Abstract Machine High-Level Abstract Primitives Low-Level Concrete Implementations Applications C + Abstract primitives C +Assembly Low-Level Abstract Machine