| 本文已被：浏览 3782次 下载 8057次 |
码上扫一扫！ |
|
|
| 基于Coq的操作系统任务管理需求层建模及验证 |
|
姜菁菁1, 乔磊1,2, 杨孟飞3, 杨桦1, 刘波1
|
|
1.北京控制工程研究所, 北京 100190;2.计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;3.中国空间技术研究院, 北京 100094
|
|
| 摘要: |
| 为确保星上操作系统中任务管理设计的可靠性，利用定理证明工具Coq对操作系统任务管理模块进行需求层建模及形式化验证.从用户角度，基于星上操作系统任务管理的基本机制，提出一种基于任务状态列表集合的验证框架.在需求层将基本机制进行形式化建模，并在Coq中实现.针对建立的需求层模型，提出6条与实际星上操作系统任务管理一致的性质并进行验证.给出其中一条性质在Coq中的验证过程，结果表明，模型满足该条性质. |
| 关键词: 任务管理 需求层 形式化建模 Coq 形式化验证 |
| DOI：10.13328/j.cnki.jos.005961 |
| 分类号: |
| 基金项目:国家自然科学基金（61632005，61502031）；中国科学院软件研究所计算机科学国家重点实验室开放课题（SYSKF1804） |
|
| Operating System Task Management Requirements Layer Modeling and Verification Based on Coq |
|
JIANG Jing-Jing1, QIAO Lei1,2, YANG Meng-Fei3, YANG Hua1, LIU Bo1
|
|
1.Beijing Institute of Control Engineering, Beijing 100190, China;2.State Key Laboratory of Computer Science(Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;3.China Academy of Space Technology, Beijing 100094, China
|
| Abstract: |
| In order to ensure the reliability of task management design in the operating system on the satellite, the theorem proving tool Coq is used to requirements layer modeling and formal verification of the operating system task management module. From the user point of view for the basic mechanism of on-board operating system task management, this study proposes verification method based on task state list collection. 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. |
| Key words: task management requirement layer formal modeling Coq formal verification |
