Formal Refinement for Operating System Kernels
The kernel of any operating system is its most critical component. The remainder of the system depends upon a correctly functioning and reliable kernel for its operation. The purpose of this book is to show that the formal specification of kernels can be followed by a completely formal refinement pr...
| Main Author: | |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
London
Springer London
2007, 2007
|
| Edition: | 1st ed. 2007 |
| Subjects: | |
| Online Access: | |
| Collection: | Springer eBooks 2005- - Collection details see MPG.ReNa |
Table of Contents:
- Introduction
- Reasons for Selecting the Examples
- Refinement Method
- Code Production
- Organisation of this Book
- Relationship to Other Work
- The Simple Kernel’s Organisation
- A Simple Kernel
- Types
- Hardware
- The Process Table.-Process Queue
- Priority Queue
- The Scheduler
- Semaphores
- Semaphore Table
- Synchronous Messages
- The Clock
- Sleepers.-User Interface
- The Separation Kernel.-Basic Architecture
- Extending the Architecture
- Summary
- An Overview of the Formal Specification
- A Separation Kernel
- Basic Types
- Hardware Issues
- Security Exits and Return Values
- The Process Table
- Process Queues
- The Scheduler
- Storage Pools
- Raw Storage
- Message Queues
- Kernel Interface-User Processes
- Devices-Trusted Code
- Process Interface to the Kernel
- Final Thoughts
- Closing Thoughts
- References
- List of Definitions