The Formal Specification And Refinement Of Open Solaris Kernel Process Based On Temporal Logic

XYZ System theory is based on Manna-Pnueli'programmed sequential logics. As a sequential logics language, XYZ/E is not only a sequential logics system, but also can represent specification of executable programms of different abstraction levels.As the engine of software developing and testifying the dependency of software, it has great academic and practical value.Formalized analysis operating system is often based on special Operating System, which makes the development and maintenance much difficult. Because of insufficient exoteric authorization, the formalized discription and analysis on general opearating system brings patent bulwalk to application. Open Solaris is a multi-task and multiuser operating system developed by Sun Company. It has the advantages of highly real-time processing, super efficiency, high availability, high performance, high security and various choices of the platform. Based on CDDL opening standard, it brings a new opportunity to operating system and industrial application.This paper describes the kernel process module of Open Solaris and the criterion of multi-task operating kernel process, the multi-task operating system kernel process based on linearity temporal logic language (TLL) XYZ/E is discribed.The establishment of kernel process,scheduling code and dynamic analysing kernel process programming is performed by using Sun DTrace; combined with software designing module, the kernel process flow chart and kernel process architecture is shown. We mainly analyse kernel process data structure,kernel process establishment,system scheduling,clock and programme all the above with XYZ/AE. Finally, kernel process criterion is desplayed; multi-task and multiuser operating system kernel process is discribed; stepwise refinement is used to refine kernel process and initial verification.