The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.11 - November (1989 vol.15)
pp: 1382-1396
ABSTRACT
<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>
INDEX TERMS
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
CITATION
W.R. Bevier, "Kit: A Study in Operating System Verification", IEEE Transactions on Software Engineering, vol.15, no. 11, pp. 1382-1396, November 1989, doi:10.1109/32.41331
18 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool