Operating System Task Management Requirements Layer Modeling and Verification Based on Coq
Author:
Affiliation:

Clc Number:

Fund Project:

National Natural Science Foundation of China (61632005, 61502031); Open project of State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (SYSKF1804)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

姜菁菁,乔磊,杨孟飞,杨桦,刘波.基于Coq的操作系统任务管理需求层建模及验证.软件学报,2020,31(8):2375-2387

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 31,2019
  • Revised:November 02,2019
  • Adopted:
  • Online: April 20,2020
  • Published: August 06,2020
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063