By Iain D. Craig MA, PhD (auth.)
The kernel of any working method is its most important part. the rest of the process depends on a accurately functioning and trustworthy kernel for its operation.
The function of this ebook is to teach that the formal specification of kernels should be through a very formal refinement method that ends up in the extraction of executable code. The formal refinement method guarantees that the code meets the specification in an exact experience.
Two kernels are unique and sophisticated. the 1st is small and of the type frequently utilized in embedded and real-time platforms. It heavily resembles the only modelled in our Formal versions of working process Kernels. the second one is a Separation Kernel, a microkernel structure devised for cryptographic and different safe functions. either kernels are sophisticated to the purpose at which executable code will be extracted. except documenting the method, together with proofs, this ebook additionally exhibits how refinement of a realistically sized specification might be undertaken.
Iain Craig is a Chartered Fellow of the BCS and has a PhD in computing device technological know-how.
Read or Download Formal Refinement for Operating System Kernels PDF
Best nonfiction_8 books
Company procedure re-engineering instruments provide thoughts to version the firm and determine possibilities to make switch. This ebook examines the methods, instruments and strategies which help remodel of the firm to accomplish global classification functionality.
The papers contained herein have been offered on the 5th overseas convention on Composite constructions (ICCS/5) held at Paisley university of expertise, Scotland in July 1989. The convention was once organised and subsidized via Paisley collage of know-how. It was once co-sponsored via the Scottish improvement employer, the nationwide Engineering Laboratory, the U.S. Air strength ecu place of work of Aerospace learn and improvement, the united states military learn, improvement and Standardisation Group-UK, Strathclyde neighborhood Council and Renfrew District Council.
Gerald P. Dwyer, Jr. and R. W. Hafer The articles and commentaries integrated during this quantity have been awarded on the Federal Reserve financial institution of St. Louis' 13th annual financial coverage convention, hung on October 21-22, 1988. The convention fascinated with the habit of asset industry costs, a subject matter of accelerating curiosity to either the preferred press and to educational journals because the bull industry of the Nineteen Eighties endured.
At the moment one of many preferred issues in biochemistry, the concept that of molecular chaperones has challenged the paradigm of protein self-assembly. Key figures in lots of disciplines overview all features of molecular chaperones during this quantity, which arises from a Royal Society dialogue assembly. evaluation chapters talk about the importance of chaperones in biochemistry, molecular genetics and phone biology.
- High Density Digital Recording
- Condensed Matter Physics: The Theodore D. Holstein Symposium
- The Release of Genetically Modified Microorganisms—REGEM 2
- The Ribonucleic Acids
- Reduced Emissions and Fuel Consumption in Automobile Engines
- Regulation of the RAS Signaling Network
Additional info for Formal Refinement for Operating System Kernels
Example text
3 The Process Table 41 AbsPTAB 1 PTAB PTAB 1 dom freech = PID \ used dom freech ∩ used = ∅ ∀ p : PID • p ∈ used ⇒ prio(p) = prio1(p) ∀ p : PID • p ∈ used ⇒ state(p) = state1(p) ∀ p : PID • p ∈ used ⇒ wakingtime(p) = wakingtime1(p) ∀ p : PID • p ∈ used ⇒ smsg(p) = smsg1(p) ∀ p : PID • p ∈ used ⇒ stacktop(p) = stacktop1(p) It is clear that the predicate of the AbsPTAB 1 schema is a function; indeed, it is an identity. Abstraction relations of this kind are extremely common. It is possible to calculate the various operations of the refinement from a functional abstraction relation and this we resist.
There are other cases in which this equivalence can be used to re-write schemata. They will be indicated and the re-written schema will be given. Therefore, given the equivalence, AddPD2 becomes 52 3 A Simple Kernel AddPD2 ∆PTAB 2 p! : PID serr ! : SYSERR pr ? : PPRIO st? : PSTATE (freehd = nullpid ∧ p! = freehd ∧ freehd = next(freehd ) ∧ p! ∈ next ∗ (| {next(freehd )} |) \ {nullpid } ∧ (p = freehd ∨ (¬ ∃ k : N • 0 < k ≤ #next ∗ (| {next(freehd )} |) \ {nullpid } ∧ next k (freehd ) = p) ∧ prio2 = prio2 ⊕ {p!
It is calculated as follows. pre FreePID2 = freehd = nullpid ∨ p?