《表3 验证结果：基于在线模型检验技术的微内核验证》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《基于在线模型检验技术的微内核验证》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

针对基于事件总线的微内核中事件总线的16个API应用所提出的框架进行了验证。对于要监测的变量运用工具设置好监测点，使用monitor＿read（）进行插桩，在操作系统运行时，应用在线模型检验器检查抽取的行为模型是否满足上述性质，实验结果如表3所示。