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

摘要：

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

关键词： 嵌入式系统 微内核 进程间通信机制 模型检测

作者: 高妍妍 李曦 周学海

作者单位: 中国科学技术大学计算机科学与技术学院, 合肥230027;中国科学技术大学苏州研究院, 苏州215123

会议类型: 国内会议

会议名称: 第三届中国计算机网络与信息安全学术会议(CCNIS2010)

会议地点: 河北保定

会议语种:中文

页码: 418-423

在线出版日期: 2010-11-26（万方平台首次上网日期，不代表论文的发表时间）