|
|||||
|
|
| L4进程间通信机制的模型检测方法 | |
| 作者姓名： | 周学海 李曦 高妍妍 |
| 摘 要： | 采用模型检测方法验证微内核操作系统的进程间通信机制,提出了一种从源码提取验证模型的方法.该方法以L4操作系统的进程间通信机制的C++源码实现为检验对象,从源码实现直接提取形式化模型,得到Promela语言的模型描述,可以直接应用模型检测器Spin对其进行正确性检测.实验表明了该方法的可行性和实用性. |
| 关 键 词： | L4微内核 进程间通信机制 模型检测 Spin |
|
||||||||||||||
|
||||||||||||||
|
||||||||||||||
|
|
|
|
| 设为首页 | 免责声明 | 关于勤云 | 加入收藏 |
|
Copyright©北京勤云科技发展有限公司 京ICP备09084417号 |