Formal Refinement for Operating System Kernels (eBook)
XV, 332 Seiten
Springer London (Verlag)
978-1-84628-967-5 (ISBN)
The kernel of any operating system is its most critical component, as the rest of the system depends on it. This book shows how the formal specification of kernels can be followed by a completely formal refinement process that leads to the extraction of executable code. This formal refinement process ensures that the code precisely meets the specification. The author documents the complete process, including proofs.
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.
Preface 6
Contents 10
List of Figures 13
1 Introduction 14
1.1 Reasons for Selecting the Examples 16
1.2 Refinement Method 20
1.3 Code Production 22
1.4 Organisation of this Book 23
1.5 Relationship to Other Work 23
2 The Simple Kernel’s Organisation 24
3 A Simple Kernel 32
3.1 Types 32
3.2 Hardware 36
3.3 The Process Table 41
3.4 Process Queue 69
3.5 Priority Queue 83
3.6 The Scheduler 113
3.7 Semaphores 132
3.8 Semaphore Table 139
3.9 Synchronous Messages 154
3.10 The Clock 171
3.11 Sleepers 174
3.12 User Interface 201
4 The Separation Kernel 216
4.1 Basic Architecture 216
4.2 Extending the Architecture 218
4.3 Summary 219
4.4 An Overview of the Formal Specification 220
5 A Separation Kernel 223
5.1 Basic Types 223
5.2 Hardware Issues 227
5.3 Security Exits and Return Values 230
5.4 The Process Table 231
5.5 Process Queues 251
5.6 The Scheduler 254
5.7 Storage Pools 263
5.8 Raw Storage 276
5.9 Message Queues 281
5.10 Kernel Interface – User Processes 298
5.11 Devices—Trusted Code 311
5.12 Process Interface to the Kernel 325
5.13 Final Thoughts 328
6 Closing Thoughts 329
References 335
List of Definitions 336
Erscheint lt. Verlag | 18.7.2007 |
---|---|
Zusatzinfo | XV, 332 p. |
Verlagsort | London |
Sprache | englisch |
Themenwelt | Mathematik / Informatik ► Informatik ► Betriebssysteme / Server |
Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge | |
Mathematik / Informatik ► Informatik ► Software Entwicklung | |
Schlagworte | Kernel • kernels • operating system • Refinement • security • Separation Kernel • user interface |
ISBN-10 | 1-84628-967-X / 184628967X |
ISBN-13 | 978-1-84628-967-5 / 9781846289675 |
Haben Sie eine Frage zum Produkt? |
![PDF](/img/icon_pdf_big.jpg)
Größe: 3,7 MB
DRM: Digitales Wasserzeichen
Dieses eBook enthält ein digitales Wasserzeichen und ist damit für Sie personalisiert. Bei einer missbräuchlichen Weitergabe des eBooks an Dritte ist eine Rückverfolgung an die Quelle möglich.
Dateiformat: PDF (Portable Document Format)
Mit einem festen Seitenlayout eignet sich die PDF besonders für Fachbücher mit Spalten, Tabellen und Abbildungen. Eine PDF kann auf fast allen Geräten angezeigt werden, ist aber für kleine Displays (Smartphone, eReader) nur eingeschränkt geeignet.
Systemvoraussetzungen:
PC/Mac: Mit einem PC oder Mac können Sie dieses eBook lesen. Sie benötigen dafür einen PDF-Viewer - z.B. den Adobe Reader oder Adobe Digital Editions.
eReader: Dieses eBook kann mit (fast) allen eBook-Readern gelesen werden. Mit dem amazon-Kindle ist es aber nicht kompatibel.
Smartphone/Tablet: Egal ob Apple oder Android, dieses eBook können Sie lesen. Sie benötigen dafür einen PDF-Viewer - z.B. die kostenlose Adobe Digital Editions-App.
Buying eBooks from abroad
For tax law reasons we can sell eBooks just within Germany and Switzerland. Regrettably we cannot fulfill eBook-orders from other countries.
aus dem Bereich