Validation of a microkernel : a case study

[摘要] ENGLISH ABSTRACT: This dissertation describes the application of formal methods to the developmentof operating systems. A related area of software engineering-the development ofprotocols-has been improved substantially by the application of formal methods. Theessential behaviour of a protocol can be checked for correctness by using a verificationsystem. A model of a protocol is developed to capture its most essential characteristics.This model is then checked automatically for correctness properties which are specifiedas temporal logic formulae.One of the most successful verification techniques is known as model checking. It isa state exploration technique, each state being the values assigned to every variablein a protocol model at a given instant. Although protocols of realistic size generatemillions of states, it is possible to check important correctness properties in minuteson a typical workstation.Broadly speaking, protocols and operating systems are similar in the sense that theyare reactive systems. Such systems are designed to interact continually with their environmentsand usually involve concurrent processing. However, there are importantdifferences 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 stepwas to select one important component and to investigate the feasibility of applyingformal methods to its development. A component that is a basic building block ofmany modern operating systems is a microkernel. It implements the https://scholar.sun.ac.za/admin/item?itemID=53247fundamentalabstractions 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 thetechniques involved, but the insight gained about the practical limits of the verificationprocess also helped the the modelling process. Since it was known from the start thatthe representation of data is important, special care was necessary to store states ascompactly as possible.This case study suggests that the designers of future operating systems can benefitfrom the use of formal methods. More important than the verification of a specificmicrokernel 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 reducethe number of states generated. However, many problems remain and these are pointedout as topics' for future research.

[发布机构] Stellenbosch University