基于Event-B的SpaceOS2操作系统任务管理
需求形式化建模与验证

doi:10.3969/j.issn.1674-1579.2014.04.011

Abstract

Abstract: With the development of space technology in China, the software applied in spacecraft becomes more complex and larger in scale.It is necessary to improve the correctness, reliability and security of software to achieve a high level. Among the approaches, the formal method is an important one.A formal method based on Event-B is introduced to describe the requirement for task model of SpaceOS2.The correctness of this model is formally guaranteed via virtual of invariants. The correctness of the model is verified by using the Rodin platform.

Key words: task management;formal model;formal verification, Event-B

CLC Number:

TAN Yan-Liang, YANG Hua, QIAO Lei. Formal Modeling and Verification of TaskManagement Requirement for SpaceOS2 Based on Event-B[J]., 2014, 40(4): 57-62.

0
/ / Recommend

Add to citation manager EndNote|Reference Manager|ProCite|BibTeX|RefWorks

URL: http://journal01.magtech.org.cn/Jwk3_kjkzjs/EN/10.3969/j.issn.1674-1579.2014.04.011

http://journal01.magtech.org.cn/Jwk3_kjkzjs/EN/Y2014/V40/I4/57

[1]	HUANG Jian-Bin, HUANG Long-Fei, HAN Xu, MENG Bo, LI Zhi, WANG Wen-Long, LI Wen. [J]. , 2018, 44(5): 30-37.
[2]	HAN Dong, HUANG Pan-Feng, LIU Xi-Yao. [J]. , 2018, 44(5): 38-46.
[3]	LIU Miao, LI Zhong-Kui. [J]. , 2018, 44(5): 47-54.
[4]	SUN Yun-Long, YUAN Chang-Qing, LI Zheng-Guang. [J]. , 2018, 44(4): 16-25.
[5]	HU Jin-Chang, ZHANG Hong-Hua, WANG Ze-Guo, CHEN Shang-Shang. [J]. , 2018, 44(4): 56-60.
[6]	SU Shao-Kan, PENG Bo, WANG Li-Wei, ZHENG Wei, CHANG Tao, CHEN Ming-Yang. [J]. , 2018, 44(4): 72-78.
[7]	ZHAO Shuang, ZHANG Ya-Sheng, DAI Hua-Yu, QI Yue- . Failure Performance and Reconstruction Method of Satellite Navigation System [J]. , 2018, 44(2): 49-55.
[8]	SUN Xiu-Qing, ZHANG Du-Zhou, WANG Li, WU Fen-Zhi. An Improved Method of Projector Calibration [J]. , 2018, 44(2): 62-66.
[9]	WANG Tong-Lei, CHEN Chao-Hui- . A Method of Analyzing and Localizing Software Vulnerability Automatically [J]. , 2018, 44(2): 73-78.
[10]	SUI Jie, CHENG Hui-Yan, YU Cheng-Wu, WU Yan-Peng, WANG Xiao-Yan, ZHENG Ran. A Thermal Stability Analysis and Simulation Method for Boresight Axis of Star Sensor [J]. , 2017, 43(4): 37-41.
[11]	LI Tao, WU Yun. Measurement Technology Based on Stereo Vision for NonCooperative Targets [J]. , 2017, 43(4): 52-56.
[12]	WU Fen-Zhi, GUO Shao-Gang, ZHU Fei-Hu, WANG Li, WU Yun, LIU Da. TwoStep Calibration Method of Lidar Sensor Based on Calibration Field [J]. , 2017, 43(4): 57-62.
[13]	CHEN Jian-Feng, YU Cheng-Wu, CHENG Hui-Yan, SUI Jie, WU Yan-Peng. An Optimal Design of Star Tracker Baffle Based on Bipod Structure [J]. , 2017, 43(4): 68-72.
[14]	CHENG Hui-Yan, ZHONG Hong-Jun, WANG Long, YANG Jun, ZHENG Ran. A Fast Algorithm of AllSky Star Map Automated Identification [J]. , 2017, 43(4): 73-78.
[15]	WANG Fei, YUAN Jian-Ping, YUAN Jing. Formation Keeping and Reconfiguration for Solar Sail Spacecraft [J]. , 2017, 43(3): 7-14.

Formal Modeling and Verification of TaskManagement Requirement for SpaceOS2 Based on Event-B

PDF (PC)

Like

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Metrics

Comments

Recommended 0