Craig Formal Refinement for Operating System Kernels

1. Auflage 2007
ISBN: 978-1-84628-967-5
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 332 Seiten

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.

Autoren/Hrsg.

Craig, Iain D.

Inhaltsverzeichnis

1;Preface;6
2;Contents;10
3;List of Figures;13
4;1 Introduction;14
4.1;1.1 Reasons for Selecting the Examples;16
4.2;1.2 Refinement Method;20
4.3;1.3 Code Production;22
4.4;1.4 Organisation of this Book;23
4.5;1.5 Relationship to Other Work;23
5;2 The Simple Kernel’s Organisation;24
6;3 A Simple Kernel;32
6.1;3.1 Types;32
6.2;3.2 Hardware;36
6.3;3.3 The Process Table;41
6.4;3.4 Process Queue;69
6.5;3.5 Priority Queue;83
6.6;3.6 The Scheduler;113
6.7;3.7 Semaphores;132
6.8;3.8 Semaphore Table;139
6.9;3.9 Synchronous Messages;154
6.10;3.10 The Clock;171
6.11;3.11 Sleepers;174
6.12;3.12 User Interface;201
7;4 The Separation Kernel;216
7.1;4.1 Basic Architecture;216
7.2;4.2 Extending the Architecture;218
7.3;4.3 Summary;219
7.4;4.4 An Overview of the Formal Specification;220
8;5 A Separation Kernel;223
8.1;5.1 Basic Types;223
8.2;5.2 Hardware Issues;227
8.3;5.3 Security Exits and Return Values;230
8.4;5.4 The Process Table;231
8.5;5.5 Process Queues;251
8.6;5.6 The Scheduler;254
8.7;5.7 Storage Pools;263
8.8;5.8 Raw Storage;276
8.9;5.9 Message Queues;281
8.10;5.10 Kernel Interface – User Processes;298
8.11;5.11 Devices—Trusted Code;311
8.12;5.12 Process Interface to the Kernel;325
8.13;5.13 Final Thoughts;328
9;6 Closing Thoughts;329
10;References;335
11;List of Definitions;336