Formal Refinement for Operating System Kernels

• Κύριος συγγραφέας: Craig, Iain D. (Συγγραφέας)
• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: London : Springer London, 2007.
• Θέματα: Computer science.; Software engineering.; Computer Science.; Software Engineering/Programming and Operating Systems.

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...

Πίνακας περιεχομένων:

• 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.