《表3 系统调用性质提取：嵌入式实时操作系统内核混合代码的自动化验证框架》

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

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

《嵌入式实时操作系统内核混合代码的自动化验证框架》

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

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

μC/OS-II内核中一共74个系统调用，分别为任务管理、内存管理、消息队列、信号量、邮箱、互斥量信号量、时间管理和事件标志等8大模块.在验证过程中，根据需求提取出每个系统调用需要满足的性质，性质是基于Hoare逻辑的形式给出的，并采用VCC提供的合约或者断言的形式，以注释的方式插入到源代码中.在系统调用的验证中，所要验证的性质大体可分为下列3个大类:类型检查、安全性和边界检查.系统调用的验证性质见表3.系统调用的8个模块列于表3的第1列中，相对应的每个模块中所验证的系统调用个数列于表的第2列，每一个模块所提取的性质列在了表的第3列.在74个系统调用中添加了共653条性质，并完成了验证.