【摘 要】
：
为确保星上操作系统中任务管理设计的可靠性,利用定理证明工具Coq对操作系统任务管理模块进行需求层建模及形式化验证.从用户角度,基于星上操作系统任务管理的基本机制,提出
【机 构】
：
北京控制工程研究所,中国空间技术研究院,计算机科学国家重点实验室（中国科学院软件研究所）
【基金项目】
：
国家自然科学基金(61632005,61502031),中国科学院软件研究所计算机科学国家重点实验室开放课题(SYSKF1804)
论文部分内容阅读
为确保星上操作系统中任务管理设计的可靠性,利用定理证明工具Coq对操作系统任务管理模块进行需求层建模及形式化验证.从用户角度,基于星上操作系统任务管理的基本机制,提出一种基于任务状态列表集合的验证框架.在需求层将基本机制进行形式化建模,并在Coq中实现.针对建立的需求层模型,提出6条与实际星上操作系统任务管理一致的性质并进行验证.给出其中一条性质在Coq中的验证过程,结果表明,模型满足该条性质.
其他文献
糖尿病肾病是糖尿病的严重并发症,在欧美国家糖尿病肾病现已成为终末期肾功能衰竭而需透析或肾移植的单个最重要原因,且其发生率仍在上升。在我国糖尿病肾病也是导致肾功能不
<正>本刊是国家批准、四川省教育厅主管、泸州医学院主办、国内外公开发行的医学类学术期刊,并且进入了国际联机检索系统,属于中国核心期刊(遴选)数据库收录期刊、中国学术期
石材行业传统转型,是以新发展理念为引领、以技术创新为驱动、以信息网络为基础平台、以数据量化管理为核心、以资源整合为途径、以智能自动为切入、以工艺流程管理为手段、
DNS为互联网应用提供名字解析服务,是互联网的重要基础服务设施.近年发生的互联网安全事件表明DNS正面临严峻的安全威胁.DNS的安全脆弱性主要包括:协议设计脆弱性、技术实现