Model Checking Research For LINUX Kernel Interprocess Communication

LINUX inherited the basic design of UNIX, and it is known as one of the operating system with great security and stability. It is an important issue that how to make the InterProcess Communication (IPC) for this kind of multi-task and multi-user system. Therefore, verification of the IPC becomes a research subject of great significance that attracts everyone's attention. Model checking is the trend to verify a system. In this paper, we use model checking to verify LINUX IPC.Pipe IPC is one of the earliest methods of communication, and its mechanism is easier than others. In this paper, part of the source code of pipe IPC was chosen to be analyzed and formalized modeled with Finite State Automaton (FSA), and then these models were translated into Promela, the input language to SPIN, to be model checked. Boundedness and terminability were verified and an improved method to the problem in pipe IPC has been worked out.Socket IPC is the second part of our research point. It is similar to pipe IPC in notion, but quite different in implementation, and more complicated. Similarly, part of the source code of socket IPC was chosen to be analyzed and formalized modeled. Before they were translated into Promela, a temporary step was taken. In order to decrease the distance between formalized model and Promela, several state transfer charts were illustrated for each state of each process. The next procedure is to translate charts to Promela, and we proposed the idea of frame, which made our Promela code model simpler and layering. Then some properties were represented by Linear-time Temporal Logic (LTL) formula, to be model checked. Some important properties such as terminability and communication completeness were valid, mean while, it indicated the feasibility of model checking IPC with SPIN. Finally, zombie process was discussed due to a result of verification.