Abstract: Microkernel architecture has become a hot topic in the research area of operating systems because of its effective isolation for modules．The multi-thread mechanism is a critical issue for the performance of the microkernel architecture．Many works research into the multi-thread of microkernel operating systems,but there are some problems such as frequent switching of system address space and high degree of implementation complexity．We used formal methods to describe and design the multi-thread and security mechanism,and proposed a hierarchical object semantics model．With the object semantics model,we formally designed the mechanism of inter-thread communication,thread scheduling,mutual exclusion and synchronization．Meanwhile,we used our self-implemented and verified microkernel operating system-VTOS as an example to test,and the results show that VTOS achieves multi-thread effectively and has a good system performance.

Key words: Microkernel,Multi-thread,Operating system,Formal description,Formal design