中国科学院研究生院学报2011，Vol.28Issue(6)：786-792,7.
L4进程间通信机制的模型检测方法
Verification of the L4 IPC implementation
摘要
Abstract
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微内核/进程间通信机制/模型检测/SpinKey words
L4 microkernel/ inter-process communication (IPC)/ model checking/ Spin分类
信息技术与安全科学引用本文复制引用
高妍妍,李曦,周学海..L4进程间通信机制的模型检测方法[J].中国科学院研究生院学报,2011,28(6):786-792,7.基金项目
国家"863"高技术研究发展计划项目(2008AA01Z101)资助 （2008AA01Z101）
