62 F.Xu et al. interrupts,and preemptive priority-based scheduling.The system APIs include "semaphores;event flags;mutual-exclusion semaphores that eliminate unbounded priority inversions;mailbores;message queues;task,time and timer manage- ment;and fired sized memory block management"[2].uC/OS-II is developed for microprocessors and microcontrollers,and it does not support virtual memory. It has been deployed in many real-world safety critical applications,including avionics (e.g.,the Mars Curiosity Rover)and medical equipments. 2.2 Overview of the Verification Framework An OS kernel hides details of the underlying hardware and provides an abstract programming model for application-level programmers.The implementation of the kernel must ensure that behaviors of user applications in the real machine are consistent with their behaviors under the abstract model 14.Thus the OS verification can be reduced to verifying refinement between the concrete and abstract programming models. Contertual Refinement as Correctness.We consider three entities,the applica- tion A,the abstract specifications of the system APIs and interrupt handlers O,and their concrete implementations O.When system calls are made or inter- rupts are handled,routines in O are invoked in the real execution,while in the programmers'mind those in O are invoked instead at the abstract level.Then the correctness of OS kernels requires O refines O under all conterts A: VA.IA[O]IC IAO]] where I-]maps a program P to the set of its observable behaviors.It says that, for all applications,executing the concrete code O does not have more observ- able behaviors than executing the abstract version O.In this paper,observable behaviors are defined as finite prefixes of execution traces consisting of observable events,following Liang et al.[17]. Contextual refinement is a very strong notion of functional correctness of system APIs since it quantifies over all applications.Moreover,it makes verifica- tion of system-wide properties simpler.For instance,if we want to verify certain property about a whole system AO,i.e.,holds over every trace in [AO], we could prove that it holds over every trace in the superset [AO]instead. Proofs at the abstract level could be much simpler than the concrete level. The Whole Verification Framework.Figure 1 shows the structure of our verifi- cation framework.To model OS kernels and applications,we introduce two lan- guages(in block A),the low-level language for the concrete code implementation and the high-level language for the abstract specification.Above them we have a program logic (in block B)that allows us to prove the low-level kernel imple- mentation contextually refines the high-level specifications.The framework also provides a set of Coq tactics (in block C)to automatically generate and prove verification conditions.The uC/OS-II modules certified in this framework are shown in block D.Below we give details of some of the building blocks.62 F. Xu et al. interrupts, and preemptive priority-based scheduling. The system APIs include “semaphores; event flags; mutual-exclusion semaphores that eliminate unbounded priority inversions; mailboxes; message queues; task, time and timer manage￾ment; and fixed sized memory block management” [2]. μC/OS-II is developed for microprocessors and microcontrollers, and it does not support virtual memory. It has been deployed in many real-world safety critical applications, including avionics (e.g., the Mars Curiosity Rover) and medical equipments. 2.2 Overview of the Verification Framework An OS kernel hides details of the underlying hardware and provides an abstract programming model for application-level programmers. The implementation of the kernel must ensure that behaviors of user applications in the real machine are consistent with their behaviors under the abstract model [14]. Thus the OS verification can be reduced to verifying refinement between the concrete and abstract programming models. Contextual Refinement as Correctness. We consider three entities, the applica￾tion A, the abstract specifications of the system APIs and interrupt handlers O, and their concrete implementations O. When system calls are made or inter￾rupts are handled, routines in O are invoked in the real execution, while in the programmers’ mind those in O are invoked instead at the abstract level. Then the correctness of OS kernels requires O refines O under all contexts A: ∀A.[[A[O]]] ⊆ [[A[O]]] where [[ ]] maps a program P to the set of its observable behaviors. It says that, for all applications, executing the concrete code O does not have more observ￾able behaviors than executing the abstract version O. In this paper, observable behaviors are defined as finite prefixes of execution traces consisting of observable events, following Liang et al. [17]. Contextual refinement is a very strong notion of functional correctness of system APIs since it quantifies over all applications. Moreover, it makes verifica￾tion of system-wide properties simpler. For instance, if we want to verify certain property Φ about a whole system A[O], i.e., Φ holds over every trace in [[A[O]]], we could prove that it holds over every trace in the superset [[A[O]]] instead. Proofs at the abstract level could be much simpler than the concrete level. The Whole Verification Framework. Figure 1 shows the structure of our verifi- cation framework. To model OS kernels and applications, we introduce two lan￾guages (in block A), the low-level language for the concrete code implementation and the high-level language for the abstract specification. Above them we have a program logic (in block B) that allows us to prove the low-level kernel imple￾mentation contextually refines the high-level specifications. The framework also provides a set of Coq tactics (in block C) to automatically generate and prove verification conditions. The μC/OS-II modules certified in this framework are shown in block D. Below we give details of some of the building blocks