Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Validation of a microkernel : a case study
Dissertation (Ph.D) -- University of Stellenbosch, 1999.
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | en_ZA |
| Published: |
Stellenbosch : Stellenbosch University
2012
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613953283063808 |
|---|---|
| access_status_str | Open Access |
| author | De Villiers, Pieter Jan Albertus |
| author2 | Holzmann, G. J. |
| author_browse | De Villiers, Pieter Jan Albertus Holzmann, G. J. |
| author_facet | Holzmann, G. J. De Villiers, Pieter Jan Albertus |
| author_sort | De Villiers, Pieter Jan Albertus |
| collection | Thesis |
| dc_rights_str_mv | Stellenbosch University |
| description | Dissertation (Ph.D) -- University of Stellenbosch, 1999. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/51539 |
| institution | Stellenbosch University (South Africa) |
| language | en_ZA |
| last_indexed | 2026-06-10T12:44:19.493Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from SUNScholar — Stellenbosch University Repository |
| publishDate | 2012 |
| publishDateRange | 2012 |
| publishDateSort | 2012 |
| publisher | Stellenbosch : Stellenbosch University |
| publisherStr | Stellenbosch : Stellenbosch University |
| record_format | dspace |
| source_str | SUNScholar — Stellenbosch University Repository |
| spelling | oai:scholar.sun.ac.za:10019.1/51539 Validation of a microkernel : a case study De Villiers, Pieter Jan Albertus Holzmann, G. J. Krzesinski, A. E. Stellenbosch University. Faculty of Science. Dept. of Computer Science. Operating systems (Computers) Computer software -- Development Software engineering Microkernel Model checking Protocols Dissertations -- Computer science Dissertation (Ph.D) -- University of Stellenbosch, 1999. 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. Doctoral 2012-08-27T11:34:33Z 2012-08-27T11:34:33Z 1999-11 Thesis http://hdl.handle.net/10019.1/51539 en_ZA Stellenbosch University 155 pages : ill. application/pdf Stellenbosch : Stellenbosch University |
| spellingShingle | Operating systems (Computers) Computer software -- Development Software engineering Microkernel Model checking Protocols Dissertations -- Computer science De Villiers, Pieter Jan Albertus Validation of a microkernel : a case study |
| title | Validation of a microkernel : a case study |
| title_full | Validation of a microkernel : a case study |
| title_fullStr | Validation of a microkernel : a case study |
| title_full_unstemmed | Validation of a microkernel : a case study |
| title_short | Validation of a microkernel : a case study |
| title_sort | validation of a microkernel a case study |
| topic | Operating systems (Computers) Computer software -- Development Software engineering Microkernel Model checking Protocols Dissertations -- Computer science |
| url | http://hdl.handle.net/10019.1/51539 |
| work_keys_str_mv | AT devillierspieterjanalbertus validationofamicrokernelacasestudy |