A Practical Verification Framework for Preemptive OS Kernels 67 (a natural number),the task status (ready,waiting,etc.and so on,depending on the low-level implementations.ctid is the name for the current task identifier t. Erample of High-Level Specifications.We use saly (Yerr(ticks)+ (ly(ticks);sched))to specify the system API "void OSTimeDly(Int16u ticks)", which delays the current task for the specified number of system ticks.The atomic operation Yerr(ticks)specifies the error case when ticks =0.ly(ticks) defines the atomic behavior of updating the status of the current task from “ready”to“waiting”with the duration set to ticks when ticks>O,and the following sched switches to another ready task,following the scheduling policy specified by the abstract scheduler x.Note that the exclusive conditions over ticks in err(ticks)and dly(ticks)make the non-deterministic choice statement deterministic.We omit the definitions of err(ticks)and dly(ticks)here. As another example,below we show the abstract scheduler specification Xuc/os-I for uC/OS-II.It requires that the selected task be ready and have the highest priority among all the ready tasks. Xuc/os-II,t.3a,pr.(tcbls)=a Aa(t)=(pr,rdy) t',pr'.(t≠t'Aa(t)=(pr',rdy)→pr'<pr 3.3 OS Correctness As we explain in Sect.2.2,the correctness of OS kernels can be defined in terms of contextual refinement.Below we give its formal definition. Definition 3.1 (OS Correctness).Oiff VA,W,W.Match(v,W,W)=((A,O),W)((A,0),W) where∈LOSFullSt→HAbsSt→Prop and Match(,(T,△，A,t),(T,△，) (t∈dom(T)A(中A)A(t=(ctid)A(dom(T)=dom((tcbls)】 The low-level kernel code O refines its high-level abstract specifications O with constraints over initial kernel states,denoted as OO,if and only if for any client code A,low-level state W and high-level state W,if W and W satisfy certain consistency constraint (w.r.t.)then the set of observable behaviors of the low-level configuration ((A,O),W)is a subset of ((A,O),W) (i.e.,(P,W)(P,W),following the event trace refinement in [17]). Due to space limit,we elide the definitions of W and W in Sects.3.1 and 3.2.The low-level whole program state W is in the form of (T,A,A,t),where the task pool T maps task identifiers to their continuations,A is the client state, A is the low-level kernel state,and t is the identifier of the current task.The high-level program state W is in the form of(T,△，)，where∑is an abstraction of the low-level kernel state A and the current task id t. The constraint Match requires that:(1)initially W and W have the same task pool T and client state A;(2)the current task t is in T;(3)the low-levelA Practical Verification Framework for Preemptive OS Kernels 67 (a natural number), the task status (ready, waiting, etc.) and so on, depending on the low-level implementations. ctid is the name for the current task identifier t. Example of High-Level Specifications. We use sdly def = (γerr(ticks) + (γdly(ticks); sched)) to specify the system API “void OSTimeDly(Int16u ticks)”, which delays the current task for the specified number of system ticks. The atomic operation γerr(ticks) specifies the error case when ticks = 0. γdly(ticks) defines the atomic behavior of updating the status of the current task from “ready” to “waiting” with the duration set to ticks when ticks > 0, and the following sched switches to another ready task, following the scheduling policy specified by the abstract scheduler χ. Note that the exclusive conditions over ticks in γerr(ticks) and γdly(ticks) make the non-deterministic choice statement deterministic. We omit the definitions of γerr(ticks) and γdly(ticks) here. As another example, below we show the abstract scheduler specification χμC/OS-II for μC/OS-II. It requires that the selected task be ready and have the highest priority among all the ready tasks. χμC/OS-II def = λΣ, t.∃α, pr.Σ(tcbls) = α ∧ α(t)=(pr,rdy)∧ ∀t , pr .(t=t ∧α(t )=(pr ,rdy))→pr ≺pr 3.3 OS Correctness As we explain in Sect. 2.2, the correctness of OS kernels can be defined in terms of contextual refinement. Below we give its formal definition. Definition 3.1 (OS Correctness). O ψ O iff ∀A, W,W. Match(ψ, W,W) =⇒ ((A, O), W) ((A, O),W) where ψ ∈ LOSFullSt → HAbsSt → Prop and Match(ψ,(T, Δ, Λ, t),(T, Δ, Σ)) def = (t ∈ dom(T))∧(ψΛΣ)∧(t=Σ(ctid))∧(dom(T)=dom(Σ(tcbls))) The low-level kernel code O refines its high-level abstract specifications O with constraints ψ over initial kernel states, denoted as O ψ O, if and only if for any client code A, low-level state W and high-level state W, if W and W satisfy certain consistency constraint (w.r.t. ψ), then the set of observable behaviors of the low-level configuration ((A, O), W) is a subset of ((A, O),W) (i.e., (P,W) (P,W), following the event trace refinement in [17]). Due to space limit, we elide the definitions of W and W in Sects. 3.1 and 3.2. The low-level whole program state W is in the form of (T, Δ, Λ, t), where the task pool T maps task identifiers to their continuations, Δ is the client state, Λ is the low-level kernel state, and t is the identifier of the current task. The high-level program state W is in the form of (T, Δ, Σ), where Σ is an abstraction of the low-level kernel state Λ and the current task id t. The constraint Match requires that: (1) initially W and W have the same task pool T and client state Δ; (2) the current task t is in T; (3) the low-level