Overview

This book was written as a companion to my book on modelling operating system kernels. It is intended to demonstrate that the formal derivation of kernels is possible (and, actually, quite easy, or so I have found thus far). Itisimportantforthereadertounderstandthatthere?nementscontained in this book are not the only ones I have performed of microkernels. To date, I have re?ned four microkernels down to executable code and have now p- duced a kit of formally speci?ed components that can be composed to form kernels. The ?rst kernel included in this book is just one example of this work. The second kernel, the Separation Kernel, is new and was partly constructed out of the kit of parts (and the reader will see reuse in its speci?cation and re?nement) and was included for speci?c reasons that will become clear anon. Bothkernelstooklessthanthreemonths’workingtimetoproduce(theactual time is rather hard to calculate because of frequent interruptions). Previous experience in re?ning kernels also paid o? in the sense that there was l- tle revision involved in their speci?cation or re?nement; the usual process of yo-yoing between levels of the derivation was absent. This appears to be an inevitable consequence of experience.

Full Product Details

Author:   Iain D. Craig
Publisher:   Springer London Ltd
Imprint:   Springer London Ltd
Edition:   Softcover reprint of hardcover 1st ed. 2007
Dimensions:   Width: 15.50cm , Height: 1.80cm , Length: 23.50cm
Weight:   0.534kg
ISBN:  

9781849966894

ISBN 10:   1849966893
Pages:   332
Publication Date:   13 October 2010
Audience:   Professional and scholarly ,  Professional and scholarly ,  Professional & Vocational ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   In Print  
This item will be ordered in for you from one of our suppliers. Upon receipt, we will promptly dispatch it out to you. For in store availability, please contact us.

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.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions