L4进程间通信机制的模型检测方法  

Verification of the L4 IPC implementation

作　　者：高妍妍[1,2] 李曦[1,2] 周学海[1,2] 

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230027 [2]中国科学技术大学苏州研究院,苏州215123

出　　处：《中国科学院研究生院学报》2011年第6期786-792,共7页Journal of the Graduate School of the Chinese Academy of Sciences

基　　金：国家"863"高技术研究发展计划项目(2008AA01Z101)资助

摘　　要：采用模型检测方法验证微内核操作系统的进程间通信机制,提出了一种从源码提取验证模型的方法.该方法以L4操作系统的进程间通信机制的C++源码实现为检验对象,从源码实现直接提取形式化模型,得到Promela语言的模型描述,可以直接应用模型检测器Spin对其进行正确性检测.实验表明了该方法的可行性和实用性.Inter-process communication（IPC） mechanism is one of the key technologies of microkernel operating system.In this paper we present a formal method to model and verify the IPC implementation.The source code of L4 IPC implementation is translated into Abstract model which is described in Promela,and the Abstract model can be verified with Spin directly.The experimental results show the feasibility and practicality of the method.

关 键 词：L4微内核 进程间通信机制 模型检测 SPIN 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]