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

摘要

进程间通信机制是微内核操作系统的关键功能之一。本文采用模型检测方法验证微内核操作系统的进程问通信机制,提出了一种从源码提取验证模型的方法。该方法以L4操作系统的进程间通信机制的C++源码实现为检验对象,从源码实现直接提取形式化模型,得到Promela语言的模型描述,可以直接应用模型检测器Spin对其进行正确性检测。实验表明了该方法的可行性和实用性。