The Design And Formal Verification Of System Task Of VTOS

The operating system is the basis of other computer software, to ensure the safety and reliability of the entire computer system, the operating system’s high safety and reliability must be ensured. The kernel is the most important part in the operating system, so first of all we must ensure the reliability of the kernel. In a reliable kernel, we must ensure the reliability of the operations provided by the kernel to user level processes. Kernel calls are the interfaces for the user-level processes to get privileged operation provided by kernel, it is necessary to ensure the accuracy and safety of these interface functions.Formal design and validated the system is a good method which is recognized to ensure the security and reliability of the operating system. Formal methods based on strict mathematical logic, it abstracts the system to a formal system which represented by logical semetics, by the way of logical reasoning to verify the nature of the system to meet. Microkernel architecture has a strong advantage of that it reduces the kernel and provides a high modular system. In order to provide kernel privileged operations for the user-level serverand user-level device driver in microkernel architecture, we using formal methods to design a kernel-level system task.This paper’s main work follows.1. Using kernel-level process provides user servers and drivers with privileged operations, rather than by using interrupt processing approach, able to provide good scalability in the multi-coreand distributed environment. Experiments show that the using an independent process have less impact on system performance.2. In order to formal describe the behavior of system task, using the operating system automaton model which based on automata theory to describe the overall structure of system task, the establishment of a state machine model for the system tasks:including system task’s working object, the events which impact of their behaviors and the handlers for each event.3. Using Isabelle/HOL processor model, with Hoare logic, set pre-and post-conditions for the conversion function in the automata model for system task, combined with the corresponding theorem proves the correctness of the function’s semantic.