主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2020-2021年专刊出版计划 微信服务介绍 最新一期:2020年第7期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
姜菁菁,乔磊,杨孟飞,杨桦,刘波.基于Coq的操作系统任务管理需求层建模及验证.软件学报,2020,31(8):0
基于Coq的操作系统任务管理需求层建模及验证
Task Management Requirements Layer Modeling and Verification Based on Coq
投稿时间:2019-08-27  修订日期:2019-11-02
DOI:10.13328/j.cnki.jos.005961
中文关键词:  任务管理  需求层  形式化建模  Coq  形式化验证
英文关键词:task management  requirements layer  formal modeling  Coq  formal verification
基金项目:国家自然科学基金(61632005,61502031);中国科学院软件研究所计算机科学国家重点实验室开放课题基金(SYSKF1804)
作者单位E-mail
姜菁菁 北京控制工程研究所, 北京 100190  
乔磊 北京控制工程研究所, 北京 100190
中国科学院软件研究所计算机科学国家重点实验室, 北京 100190 
fly2moon@aliyun.com 
杨孟飞 中国空间技术研究院, 北京 100094  
杨桦 北京控制工程研究所, 北京 100190  
刘波 北京控制工程研究所, 北京 100190  
摘要点击次数: 590
全文下载次数: 234
中文摘要:
      为确保星上操作系统中任务管理设计的可靠性,利用定理证明工具Coq对操作系统任务管理模块进行需求层建模及形式化验证.本文从用户角度基于星上操作系统任务管理的基本机制,提出了一种基于任务状态列表集合的验证框架,在需求层将基本机制进行形式化建模并在Coq中实现,针对建立的需求层模型提出6条与实际星上操作系统任务管理一致的性质并进行验证.给出其中一条性质在Coq中的验证过程,结果表明模型满足该条性质.
英文摘要:
      In order to ensure the reliability of task management design in the operating system on the star, the theorem proving tool Coq is used to requirements layer modeling and formal verification of the operating system task management module. This article from the user point of view for the basic mechanism of on-board operating system task management, A verification method based on task state list collection is proposed. The mechanism process is formalized and implemented in Coq. Six properties are consistent with the task management of the real-world operating system for the established requirements layer model. This article gives a verification process of one of the properties in Coq. The result shows that the model satisfies the properties of the article.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利