Analysis And Test Generation Based On Property Of Minix3 Operating System

Minix operating system is a multi-user, multi-mission and a Unix-like operating system, which runs in the PC. Minix3 is a new open-source microkernel operating system, which is loosely base on previous versions of Minix. The system removes many services of the OS from the kernel. The number of the kernel codes is less than previous versions of Minix. Compared with other OS, the architecture of Minix3 possess many advantages, such as higher reliability, higher security and easy to be extended. Minix system is designed based on modular and hierarchical idea. This structure allows us to replace other different file systems with entire file system much easier, and without recompiling the kernel of Minix3. Property-based testing pays attention on the property which needs to be tested in the system. The chosed property could be only one or more. So the testing work can be reduced and the testing efficiency can be improved. Meanwhile, error properties can be joined the set of the property. So, reliability of the test results can be improved.In this thesis, the work of the analysis and test generation of Minix3 based on property have been studying, mainly research work is elaborated as follows:Firstly, we analyzed the characteristics of microkernel operating system, the architecture of Minix3 and the improvement in its structure. We read the Minix3.1.1 source code seriously and analyzed the functionalities which are implemented by the corresponding code in depth.Secondly, we make the definition of property to Minix3 operating system. The Petri net models of the 28 kernel callings based on property are built, and its model is further abstracted. Some functional models are described by Visio or CPN.Thirdly, we studied the relations between program slicing and property modeling. We find a test generation approach from combining property modeling and program slicing, and proposed the test generation system based on above method. Meanwhile, we also considered the application of program slicing in the software reuse.Finally, we have been doing the white-box testing, black-box testing and the testing based on property respectively to the important program of Minix3 system. The test result and test case are given partly. Meanwhile, summary and category of property library based on property are given.In order to reduce the complexity of software model, We will consider the granularity of slicing and other higher level abstract modeling method, and draw up the standards of their levels of abstraction. In the future, we will provide the formal definition of property and do research on test coverage to make the high-quality analysis and test.