A Practical Verification Framework for Preemptive OS Kernels 63 Multi-Level Priority-Based Interrupts Message Queue Mutex Semaphore Mail Box Scheduler (Timer &... Synchronization Mechanisms D.Verifying uC/Os-II Relational Assertions Refinement-Based Program Logic Contextual Refinement Entailment B.Refinement-Based Verification ●】 Forward Reasoning for Refinement-Based The High-Level Language System-Wide Judgements High-Level Small-Step Operational Semantics Properties with Configurable Schedulers Domain-Specific High-Level Abstract C Subset Low-Level Assembly Solvers Statements Primitives Low-Level Small-Step Operational Semantics with Context Switch and Interrupts The Low-Level Language C.Coq Tactics A.Modeling of oS Kernels Verification Framework Fig.1.Structure of the verification framework and uC/OS-II verification 3 Modeling of OS Kernels As explained above,the correctness of OS kernels is formalized based on three entities-user applications A,the concrete implementation O,and the abstract specification O.In this section we introduce the programming (or modeling) languages for the three entities (see block A in Fig.1).Due to space limit,we only show the main language features with simplifications for clear presentation. The details are available at TR and the Cog code [26]. 3.1 The Low-Level Language The low-level language consists of two parts for implementations of user appli- cations and OS kernels,respectively. Application Language.The application language is shown at the top of Fig.2. It is a subset of the C language consisting of function calls,pointer operations (except pointer arithmetics),arrays,structs,bit operations,etc.The application code A maps function names to their function bodies.The command f(e)calls the function f,which could be either an application function in A or an OS API (in O at the low-level or in O at the high-level,as we explain below).A Practical Verification Framework for Preemptive OS Kernels 63 Fig. 1. Structure of the verification framework and μC/OS-II verification 3 Modeling of OS Kernels As explained above, the correctness of OS kernels is formalized based on three entities — user applications A, the concrete implementation O, and the abstract specification O. In this section we introduce the programming (or modeling) languages for the three entities (see block A in Fig. 1). Due to space limit, we only show the main language features with simplifications for clear presentation. The details are available at TR and the Coq code [26]. 3.1 The Low-Level Language The low-level language consists of two parts for implementations of user appli￾cations and OS kernels, respectively. Application Language. The application language is shown at the top of Fig. 2. It is a subset of the C language consisting of function calls, pointer operations (except pointer arithmetics), arrays, structs, bit operations, etc. The application code A maps function names to their function bodies. The command f(¯e) calls the function f, which could be either an application function in A or an OS API (in O at the low-level or in O at the high-level, as we explain below)