Name
Abstract | ||
|---|---|---|
We propose a practical verification framework for preemptive OS kernels. The framework models the correctness of API implementations in OS kernels as contextual refinement of their abstract specifications. It provides a specification language for defining the high-level abstract model of OS kernels, a program logic for refinement verification of concurrent kernel code with multi-level hardware interrupts, and automated tactics for developing mechanized proofs. The whole framework is developed for a practical subset of the C language. We have successfully applied it to verify key modules of a commercial preemptive OS mu C/OS-II [ 2], including the scheduler, interrupt handlers, message queues, and mutexes etc. We also verify the priority-inversion-freedom (PIF) in mu C/OS-II. All the proofs are mechanized in Coq. To our knowledge, our work is the first to verify the functional correctness of a practical preemptive OS kernel with machine-checkable proofs. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-41540-6_4 | COMPUTER AIDED VERIFICATION: 28TH INTERNATIONAL CONFERENCE, CAV 2016, PT II |
Field | DocType | Volume |
Kernel (linear algebra),Specification language,Interrupt,Programming language,Computer science,Interrupt handler,Correctness,Implementation,Theoretical computer science,Message queue,Mathematical proof | Conference | 9780 |
ISSN | Citations | PageRank |
0302-9743 | 7 | 0.72 |
References | Authors | |
12 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Fengwei Xu | 1 | 7 | 0.72 |
| Ming Fu | 2 | 84 | 6.86 |
| Xinyu Feng | 3 | 443 | 30.52 |
| Xiaoran Zhang | 4 | 7 | 0.72 |
| Hui Zhang | 5 | 20 | 3.20 |
| Zhaohui Li | 6 | 7 | 0.72 |