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

• 作者: 周学海 李曦 高妍妍
• 来源期刊: 中国科学院研究生院学报
• 学科: 工学
• 关键词: L4微内核 进程间通信机制 模型检测 Spin
• 年，卷（期）: 2011,（6）
• 所属期刊栏目: 论文
• 页码范围: 786-792
• 分类号: TP302
• 字数: 6608字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李曦	中国科学技术大学计算机科学与技术学院	119	751	13.0	21.0
5	周学海	中国科学技术大学计算机科学与技术学院	109	885	17.0	24.0
9	高妍妍	中国科学技术大学计算机科学与技术学院	11	24	3.0	4.0