基于时间自动机的操作系统中断管理建模与验证

doi:10.3969/j.issn.1674-1579.2014.04.010

Abstract

Abstract: The temporal correctness has always been a hotspot and difficult problem in the field of space embedded software. With the theory of timed automata, the interrupt management of a certain onboard operating system and the environment interacting with it are modeled respectively to describe the whole interrupt management process. By using the modelchecking tool Uppaal, the performances of interrupt management are verified, including the reachability, the safety, the liveness and the correctness of service behavior.

Key words: interrupt management, timed automata, formal verification, modeling

CLC Number:

WANG Ruo-Chuan, YANG Meng-Fei, QIAO Lei. Modeling and Verification of Operating System Interrupt Management Based on Timed Automata[J]., 2014, 40(4): 52-56.

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.010

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

[1]	QIU Zhicheng, DU Jiahao. Simulation of Multiple Flexible Beams Vibration Control Based on Fuzzy Reinforcement Learning [J]. Aerospace Contrd and Application, 2021, 47(1): 29-39.
[2]	TANG Ning, LIU Zhi-Yong, GAO Ya-Nan, HE Ying-Zi. Design and Analysis of DFT of Spacecraft Control System Based on Byzantine Fault Tolerant Architecture [J]. , 2017, 43(5): 55-60.
[3]	ZHOU Yu-Kui, YANG Hua, QIAO Lei. Formal Modeling and Verification Method of InterruptManagement Requirement and Design Based on EventB [J]. , 2017, 43(3): 71-78.
[4]	WANG You-Yi, TANG Liang, HE Ying-Zi. Dynamic Modeling and Decoupled Control of Ultra Quiet Platform [J]. , 2016, 42(4): 6-.
[5]	LIN Qian, YUAN Jun. Dynamic Modeling and Simulation of Flexible Space Manipulator Based on Vector Pairs Method [J]. , 2016, 42(2): 26-31.
[6]	JIANG Hong, YANG Meng-Fei, YU Guang-Liang, WEI Meng-Jie. An Approach for Functional Level Power Estimation of Onboard Computer [J]. , 2015, 41(3): 48-52.
[7]	WEI Yan-Ming, GENG Jin-Yue, HE Qing-Song, WANG Hai-Xing. Simulation Analysis on the LowPower Nitrogen/Hydrogen Mixtures Arcjets [J]. , 2015, 41(1): 1-8.
[8]	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.
[9]	LIU Bao-Yu, JIN Lei, JIA Ying-Hong. Dynamics Fine Modeling and Simulation of LargeScale Control Moment Gyro [J]. , 2014, 40(1): 21-26.
[10]	ZHANG Jun ^1,2, HU Haixia ^1.2, XING Yan ^1,2. Backstepping Controller Design for Space Robot [J]. , 2009, 35(1): 7-12.
[11]	TIAN Lin, XU Shijie. Research on Attitude Dynamics Modeling and Control for Spin-Stabilized Micro-Satellite [J]. , 2009, 35(1): 47-50.
[12]	GAO Wei ^1,2, XING Yan ^1,2, WANG Nanhua^1,2. Review of Fault Diagnosis Approach Based on Qualitative Model [J]. , 2009, 35(1): 25-29.

Modeling and Verification of Operating System Interrupt Management Based on Timed Automata

PDF (PC)

Like

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 12

Metrics

Comments

Recommended 0