基于Coq的操作系统任务管理需求层建模及验证

来源：软件学报杂志2020年第8期北京时间：

作者：姜菁菁，乔磊，杨孟飞，杨桦，刘波

单位：姜菁菁，北京控制工程研究所, 北京 10019011,乔磊，北京控制工程研究所, 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 10019002,杨孟飞，中国空间技术研究院, 北京 10009403,杨桦，北京控制工程研究所, 北京 10019004,刘波，北京控制工程研究所, 北京 10019005

摘要：为确保星上操作系统中任务管理设计的可靠性，利用定理证明工具Coq对操作系统任务管理模块进行需求层建模及形式化验证.从用户角度，基于星上操作系统任务管理的基本机制，提出一种基于任务状态列表集合的验证框架.在需求层将基本机制进行形式化建模，并在Coq中实现.针对建立的需求层模型，提出6条与实际星上操作系统任务管理一致的性质并进行验证.给出其中一条性质在Coq中的验证过程，结果表明，模型满足该条性质.

关键词：任务管理;需求层;形式化建模;Coq;形式化验证

基金资助：国家自然科学基金（61632005，61502031）；中国科学院软件研究所计算机科学国家重点实验室开放课题（SYSKF1804）