《表1 Coq代码行统计：基于Coq的操作系统任务管理需求层建模及验证》
提示：宽带有限、当前游客访问压缩模式
在Coq中对模型进行第2.3.1节中的4条性质的验证，结果表明，在Coq中建立的模型满足4条性质.具体的代码统计见表1.
| 图表编号 | XD00153542200 严禁用于非法目的 |
|---|---|
| 绘制时间 | 2020.08.01 |
| 作者 | 姜菁菁、乔磊、杨孟飞、杨桦、刘波 |
| 绘制单位 | 北京控制工程研究所、北京控制工程研究所、计算机科学国家重点实验室(中国科学院软件研究所)、中国空间技术研究院、北京控制工程研究所、北京控制工程研究所 |
| 更多格式 | 高清、无水印（增值服务） |
