论文部分内容阅读
LINUX操作系统继承了UNIX的基本设计思想,是当今为人们所公认的具有较强的安全性和稳定性的系统。对于这样一种多任务、多用户的操作系统来说,怎样进行进程间通信(InterProcess Communication, IPC),是个不可忽视的重大问题。对进程间通信的正确性的验证,成为一个值得共同关注的有着相当意义的研究课题。模型检测现已成为验证系统的趋势,本文正是采用了这种方法对LINUX进程间通信进行验证。管道进程间通信作为最早的通信方式之一,通信机制相对而言较为简单。本文首先对LINUX内核2.6.0版本中管道通信的相关源代码进行分析,抽取出用有限状态自动机(Finite State Automaton, FSA)描述的形式化模型,继而向Promela代码转换。随后采用线性时序逻辑(Linear-time Temporal Logic, LTL)公式表达期望系统满足的属性,通过Xspin工具进行模型检测,验证了系统的有界性和可终止性,并就实际进程间通信中容易发生的问题提出了改进方案。Socket进程间通信是本文的第二个研究重点,从概念上说,与管道通信比较相似,但实现上相距甚远,也更为复杂,是能够应用于非近亲进程之间的通信方式。研究了LINUX内核中与socket相关的源代码,抽取服务器端和客户端的形式化模型。将形式化模型转换成Promela代码之前,添加了一个中间步骤:为每个进程的每个状态建立状态转换表,缩小形式化模型与Promela代码的差距。在向Promela代码转换的过程中,本文提出了搭建框架的思想,使得建立代码模型更加简单化、层次化。期望系统满足的属性同样使用LTL公式表达,再输入模型检测工具,验证了系统的可终止性和通信完整性等重要性质,同时也说明SPIN对于进程间通信领域的可行性。最后由一个验证结果展开对僵尸进程的探讨。