| 000 -LEADER |
|---|
| fixed length control field |
03309nam a22004215i 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
978-1-84628-967-5 |
| 003 - CONTROL NUMBER IDENTIFIER |
|---|
| control field |
DE-He213 |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20161121230613.0 |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION |
|---|
| fixed length control field |
cr nn 008mamaa |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
100301s2007 xxk| s |||| 0|eng d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9781846289675 |
| -- |
978-1-84628-967-5 |
| 024 7# - OTHER STANDARD IDENTIFIER |
|---|
| Standard number or code |
10.1007/978-1-84628-967-5 |
| Source of number or code |
doi |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER |
|---|
| Classification number |
QA76.758 |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
UMZ |
| Source |
bicssc |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
UL |
| Source |
bicssc |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
COM051230 |
| Source |
bisacsh |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
005.1 |
| Edition number |
23 |
| 100 1# - MAIN ENTRY--PERSONAL NAME |
|---|
| Personal name |
Craig, Iain D. |
| Relator term |
author. |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Formal Refinement for Operating System Kernels |
| Medium |
[electronic resource] / |
| Statement of responsibility, etc. |
by Iain D. Craig. |
| 264 #1 - PRODUCTION, PUBLICATION, DISTRIBUTION, MANUFACTURE, AND COPYRIGHT NOTICE |
|---|
| Place of production, publication, distribution, manufacture |
London : |
| Name of producer, publisher, distributor, manufacturer |
Springer London, |
| Date of production, publication, distribution, manufacture, or copyright notice |
2007. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
XV, 332 p. |
| Other physical details |
online resource. |
| 336 ## - CONTENT TYPE |
|---|
| Content type term |
text |
| Content type code |
txt |
| Source |
rdacontent |
| 337 ## - MEDIA TYPE |
|---|
| Media type term |
computer |
| Media type code |
c |
| Source |
rdamedia |
| 338 ## - CARRIER TYPE |
|---|
| Carrier type term |
online resource |
| Carrier type code |
cr |
| Source |
rdacarrier |
| 347 ## - DIGITAL FILE CHARACTERISTICS |
|---|
| File type |
text file |
| Encoding format |
PDF |
| Source |
rda |
| 505 0# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
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. |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc. |
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 process that leads to the extraction of executable code. The formal refinement process ensures that the code meets the specification in a precise sense. Two kernels are specified and refined. The first is small and of the kind often used in embedded and real-time systems. It closely resembles the one modelled in our Formal Models of Operating System Kernels. The second is a Separation Kernel, a microkernel architecture devised for cryptographic and other secure applications. Both kernels are refined to the point at which executable code can be extracted. Apart from documenting the process, including proofs, this book also shows how refinement of a realistically sized specification can be undertaken. Iain Craig is a Chartered Fellow of the BCS and has a PhD in Computer Science. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name entry element |
Computer science. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name entry element |
Software engineering. |
| 650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name entry element |
Computer Science. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name entry element |
Software Engineering/Programming and Operating Systems. |
| 710 2# - ADDED ENTRY--CORPORATE NAME |
|---|
| Corporate name or jurisdiction name as entry element |
SpringerLink (Online service) |
| 773 0# - HOST ITEM ENTRY |
|---|
| Title |
Springer eBooks |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY |
|---|
| Relationship information |
Printed edition: |
| International Standard Book Number |
9781846289668 |
| 856 40 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Uniform Resource Identifier |
http://dx.doi.org/10.1007/978-1-84628-967-5 |
| 912 ## - |
|---|
| -- |
ZDB-2-SCS |
