Validation of a microkernel : a case study
Date
1999-11
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : Stellenbosch University
Abstract
ENGLISH ABSTRACT: This dissertation describes the application of formal methods to the development
of operating systems. A related area of software engineering-the development of
protocols-has been improved substantially by the application of formal methods. The
essential behaviour of a protocol can be checked for correctness by using a verification
system. A model of a protocol is developed to capture its most essential characteristics.
This model is then checked automatically for correctness properties which are specified
as temporal logic formulae.
One of the most successful verification techniques is known as model checking. It is
a state exploration technique, each state being the values assigned to every variable
in a protocol model at a given instant. Although protocols of realistic size generate
millions of states, it is possible to check important correctness properties in minutes
on a typical workstation.
Broadly speaking, protocols and operating systems are similar in the sense that they
are reactive systems. Such systems are designed to interact continually with their environments
and usually involve concurrent processing. However, there are important
differences between protocols and operating systems. For example, in protocol verification,
the focus is on the transmission rules. Data can be represented more abstractly.
For operating systems, this is not so. Data structures (such as a scheduler queue)
represent the internal state of the system and must be represented in more detail.
To verify a complete operating system is a formidable task. A manageable first step
was to select one important component and to investigate the feasibility of applying
formal methods to its development. A component that is a basic building block of
many modern operating systems is a microkernel. It implements the https://scholar.sun.ac.za/admin/item?itemID=53247fundamental
abstractions which support the rest of the system.
Instead of using an existing verification system, an experimental verification system was developed to verify the microkernel. This was done primarily to learn about the
techniques involved, but the insight gained about the practical limits of the verification
process also helped the the modelling process. Since it was known from the start that
the representation of data is important, special care was necessary to store states as
compactly as possible.
This case study suggests that the designers of future operating systems can benefit
from the use of formal methods. More important than the verification of a specific
microkernel is the general approach, which could be used to verify similar systems.
The experience gained from this case study is presented as a list of guidelines to reduce
the number of states generated. However, many problems remain and these are pointed
out as topics' for future research.
AFRIKAANSE OPSOMMING: Hierdie verhandeling beskryf die toepassing van formele metodes om bedryfstelsels te ontwikkel. 'n Verwante gebied-die ontwikkeling van protokolle-is reeds beduidend verbeter deur die gebruik van formele metodes. Die basiese gedrag van 'n protokol kan nagegaan word vir korrektheid deur, 'n verikasiestelsel te gebruik. 'n Model van 'n protokol word ontwikkel om die belangrikste gedragspatrone vas te yang. Die model word dan outomaties analiseer om sekere korrektheidseienskappe na te gaan wat gespesifiseer word as formules intemporal logika. Een van die mees suksesvolle verifikasietegnieke staan bekend as modeltoetsing ( "model checking"). Die tegniek behels 'n soektog waar toestande sistematies ondersoek word. Elke toestand is die gesamentlike waardes wat toegewys is aan elke veranderlike van 'n modelop 'n gegewe tydstip. Alhoewel protokolle van realistiese grootte miljoene state kan genereer, is dit moontlik om belangrike korrektheidseinskappe na te gaan in enkele minute op 'n tipiese persoonlike rekenaar. Breedweg is protokolle en bedryfstelsels soortgelyk in die sin dat beide reaktiewe stelsels is. Sulke stelsels word ontwerp vir kontinue interaksie met hulle omgewings en behels gewoonlik gelyklopende verwerking. Nogtans is daar belangrike verskille tussen protokolle en bedryfstelsels. Byvoorbeeld, in die verifikasie van protokolle is die klem op transmissiereels. Data kan meer abstrak voorgestel word. Vir bedryfstelsels is dit nle so nie. Datastrukture (soos 'n skeduleerdertou) verteenwoordig die interne toestand van die stelsel en moet in meer detail voorgestel word. Om 'n volledige bedryfstelsel te verifieer is 'n geweldige taak. As 'n hanteerbare eerste stap is een belangrike komponent geselekteer. Die doel was om vas te stel of dit haalbaar sou wees om formele metodes te gebruik om so 'n komponent te ontwikkel. 'n Mikrokern is 'n 'n basiese boublok van baie moderne bedryfstelsels. Dit implementeer die fundamentele abstraksies wat die res van die stelsel ondersteun. In plaas daarvan om 'n bestaande verifikasiestelsel te gebruik, is 'n eksperimentele stelsel ontwikkel om die mikrokern te verifieer. Dit is gedoen hoofsaaklik om meer te leer van die betrokke tegnieke, maar die insig wat bekom is aangaande die praktiese beperkings van die verifikasieproses het ook gehelp tydens modellering. Omdat dit bekend was dat die voorstelling van data belangrik is, is spesiale aandag geskenk aan die kompakte voorstelling van toestande. Die gevallestudie toon aan dat die ontwerpers van toekomstige bedryfstelsels voordeel kan trek uit die gebruik vanformele metodes. Belangriker as die verifikasie van 'n spesifieke mikrokern, is die algemene benadering wat moontlik aangewend kan word om soortgelyke stelsels te verifieer. Die ondervinding wat opgedoen is tydens die projek word aangebied as 'n lys van riglyne om die aantal toestande wat genereer word te verminder. Heelwat probleme bly nog oor en word uitgewys as onderwerpe vir verdere navorsing.
AFRIKAANSE OPSOMMING: Hierdie verhandeling beskryf die toepassing van formele metodes om bedryfstelsels te ontwikkel. 'n Verwante gebied-die ontwikkeling van protokolle-is reeds beduidend verbeter deur die gebruik van formele metodes. Die basiese gedrag van 'n protokol kan nagegaan word vir korrektheid deur, 'n verikasiestelsel te gebruik. 'n Model van 'n protokol word ontwikkel om die belangrikste gedragspatrone vas te yang. Die model word dan outomaties analiseer om sekere korrektheidseienskappe na te gaan wat gespesifiseer word as formules intemporal logika. Een van die mees suksesvolle verifikasietegnieke staan bekend as modeltoetsing ( "model checking"). Die tegniek behels 'n soektog waar toestande sistematies ondersoek word. Elke toestand is die gesamentlike waardes wat toegewys is aan elke veranderlike van 'n modelop 'n gegewe tydstip. Alhoewel protokolle van realistiese grootte miljoene state kan genereer, is dit moontlik om belangrike korrektheidseinskappe na te gaan in enkele minute op 'n tipiese persoonlike rekenaar. Breedweg is protokolle en bedryfstelsels soortgelyk in die sin dat beide reaktiewe stelsels is. Sulke stelsels word ontwerp vir kontinue interaksie met hulle omgewings en behels gewoonlik gelyklopende verwerking. Nogtans is daar belangrike verskille tussen protokolle en bedryfstelsels. Byvoorbeeld, in die verifikasie van protokolle is die klem op transmissiereels. Data kan meer abstrak voorgestel word. Vir bedryfstelsels is dit nle so nie. Datastrukture (soos 'n skeduleerdertou) verteenwoordig die interne toestand van die stelsel en moet in meer detail voorgestel word. Om 'n volledige bedryfstelsel te verifieer is 'n geweldige taak. As 'n hanteerbare eerste stap is een belangrike komponent geselekteer. Die doel was om vas te stel of dit haalbaar sou wees om formele metodes te gebruik om so 'n komponent te ontwikkel. 'n Mikrokern is 'n 'n basiese boublok van baie moderne bedryfstelsels. Dit implementeer die fundamentele abstraksies wat die res van die stelsel ondersteun. In plaas daarvan om 'n bestaande verifikasiestelsel te gebruik, is 'n eksperimentele stelsel ontwikkel om die mikrokern te verifieer. Dit is gedoen hoofsaaklik om meer te leer van die betrokke tegnieke, maar die insig wat bekom is aangaande die praktiese beperkings van die verifikasieproses het ook gehelp tydens modellering. Omdat dit bekend was dat die voorstelling van data belangrik is, is spesiale aandag geskenk aan die kompakte voorstelling van toestande. Die gevallestudie toon aan dat die ontwerpers van toekomstige bedryfstelsels voordeel kan trek uit die gebruik vanformele metodes. Belangriker as die verifikasie van 'n spesifieke mikrokern, is die algemene benadering wat moontlik aangewend kan word om soortgelyke stelsels te verifieer. Die ondervinding wat opgedoen is tydens die projek word aangebied as 'n lys van riglyne om die aantal toestande wat genereer word te verminder. Heelwat probleme bly nog oor en word uitgewys as onderwerpe vir verdere navorsing.
Description
Dissertation (Ph.D) -- University of Stellenbosch, 1999.
Keywords
Operating systems (Computers), Computer software -- Development, Software engineering, Microkernel, Model checking, Protocols, Dissertations -- Computer science