Department of Computer Science

Permanent URI for this community

https://scholar.sun.ac.za/handle/10019.1/96336

Browse

Browsing Department of Computer Science by browse.metadata.advisor "Holzmann, G. J."

Now showing 1 - 1 of 1
  • Thumbnail Image
    Item
    Validation of a microkernel : a case study
    (Stellenbosch : Stellenbosch University, 1999-11) De Villiers, Pieter Jan Albertus; Holzmann, G. J.; Krzesinski, A. E.; Stellenbosch University. Faculty of Science. Dept. of Computer Science.
    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.