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

• 作者: 乔磊 刘波 姜菁菁 杨孟飞 杨桦
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 任务管理 需求层 形式化建模 Coq 形式化验证
• 年，卷（期）: 2020,（8）
• 所属期刊栏目: 面向新兴系统的形式化建模与验证方法专题
• 页码范围: 2375-2387
• 页数: 13页
• 分类号: TP306
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005961

摘要

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