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

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: https://journal01.magtech.org.cn/Jwk3_kjkzjs/EN/10.3969/j.issn.1674-1579.2014.04.010

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

[1]	ZHANG Yubo, WANG Lintao, LI Lin, WANG Xiaoming, XU Zhenbang, CHEN Yang. Low Frequency Vibration Isolator Driven by Piezoelectric Ceramics [J]. Aerospace Contrd and Application, 2025, 51(1): 25-32.
[2]	CAI Chensheng, ZHU Qinghua, TANG Yucong, ZHANG Yanquan. Spacecraft Control and Simulation Technology Based on Multi Physical Field Coupling Modeling [J]. Aerospace Contrd and Application, 2024, 50(5): 84-91.
[3]	CHEN Yizhi, YU Qiang, LYU Jing, LI Qing, GUO Jianxin, WANG Tianshu. Equivalent Modeling Methods for Liquid Sloshing in High-Orbit Large Spacecraft [J]. Aerospace Contrd and Application, 2024, 50(5): 77-83.
[4]	TANG Qingyuan, ZHANG Yuyuan. Reliability Design and Verification of A Model Based Universalized Spacecraft [J]. Aerospace Contrd and Application, 2024, 50(3): 77-85.
[5]	SHI Yongkang, WANG Yao, ZOU Nan, YU Chao, LI Liang, LI Peng. Design and Practice of Model Conversion Method of Multibody Mechanical Systems Based on Simulink [J]. Aerospace Contrd and Application, 2023, 49(1): 90-97.
[6]	SONG Xiaojuan, LI Xuesong, HE Xiaodong, LYU Shufeng. Hybrid Adaptive Attitude Maneuver Control for Flexible Liquid Filled Spacecraft [J]. Aerospace Contrd and Application, 2023, 49(1): 11-20.
[7]	YANG Chao, ZHOU Qingrui, WANG Hui. Modeling and Optimization Algorithm of Multi Task Assignment for Multi Satellite [J]. Aerospace Contrd and Application, 2022, 48(5): 39-46.
[8]	CAI Yaxing, WANG Xinglong, ZHU Yuehe. On orbit service mission modeling and reinforcement learning service sequence planning in GEO [J]. Aerospace Contrd and Application, 2022, 48(3): 39-48.
[9]	ZHU Yuqi, XIANG Guofei, MA Congjun, YOU Xingxing, DIAN Songyi. Trajectory tracking control and disturbance rejection strategy for continuum robots with improved modeling method [J]. Aerospace Contrd and Application, 2022, 48(2): 29-38.
[10]	ZHOU B C, LI Y. Observability analysis for autonomous orbit determination using inter satellite measurement with modelling errors [J]. Aerospace Contrd and Application, 2022, 48(2): 8-17.
[11]	ZHAO Tongshuang, ZHANG Jiyang, WANG Yingguang, FAN Yahong, LUO Ruizhi. Modeling and Decoupling Control Method of Magnetically Levitated Rotary Joints [J]. Aerospace Contrd and Application, 2022, 48(2): 71-79.
[12]	LI Shaofeng, YANG Mengfei, QIAO Lei, JIANG Jingjing, WANG Tingyu. Requirement Level Verification of File System for Spacecraft [J]. Aerospace Contrd and Application, 2022, 48(2): 62-70.
[13]	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.
[14]	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.
[15]	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.

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 15

Metrics

Comments

Recommended 10