Issue No. 11 - November (1989 vol. 15)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.41331
<p>The author reviews Kit, a small multitasking operating system kernel written in the machine language of a uniprocessor von Neumann computer. The kernel is proved to implement on this shared computer a fixed number of conceptually distributedcommunicating processes. In addition to implementing processes, the kernel provides the following verified services: process scheduling, error handling, message passing, and an interface to asynchronous devices. As a by-product of the correctness proof, security-related results such as the protection of the kernel from tasks and the inability of tasks to enter supervisor mode are proved. The problem is stated in the Boyer-Moore logic, and the proof is mechanically checked with the Boyer-Moore theorem prover.</p>
verification; Kit; multitasking operating system kernel; machine language; uniprocessor von Neumann computer; conceptually distributed communicating processes; process scheduling; error handling; message passing; interface; asynchronous devices; correctness proof; security-related results; supervisor mode; Boyer-Moore logic; Boyer-Moore theorem prover; multiprogramming; operating systems (computers); program verification; theorem proving
W. Bevier, "Kit: A Study in Operating System Verification," in IEEE Transactions on Software Engineering, vol. 15, no. , pp. 1382-1396, 1989.