Event-B interpretation for space aircraft description language model

doi:10.3724/SP.J.1087.2012.03525

Journal of Computer Applications ›› 2012, Vol. 32 ›› Issue (12): 3525-3528.DOI: 10.3724/SP.J.1087.2012.03525

• Computer software technology • Previous Articles Next Articles

Event-B interpretation for space aircraft description language model

QI Yan-xia¹,SHEN Hui-li²,CHEN Zhao-hui¹,GU Bin¹

1. Beijing Institute of Control Engineering, Beijing 100080,China
2. School of Software Engineering, East China Normal University, Shanghai 200062,China

Received:2012-06-28 Revised:2012-08-29 Online:2012-12-29 Published:2012-12-01
Contact: SHEN Hui-li

SPARDL模型的Event-B解释

綦艳霞¹,沈慧丽²,陈朝晖¹,顾斌¹

1. 北京控制工程研究所，北京 100080
2. 华东师范大学软件学院，上海 200062

通讯作者: 沈慧丽
作者简介:綦艳霞（1974-），女，北京人，工程师，博士，主要研究方向：嵌入式软件；〓沈慧丽（1990-），女，上海人，主要研究方向：程序分析与验证；〓陈朝晖（1965-），男，北京人，研究员，硕士，主要研究方向：嵌入式软件；〓顾斌（1968-），男，北京人，研究员，硕士，主要研究方向：嵌入式软件。
基金资助:
国家自然科学基金资助项目

Abstract

Abstract: A requirement modeling language called SPARDL was proposed for modeling and analyzing such periodic control systems consisting of periodic behaviors together with the mode transition mechanism. The Event-B interpretation was specified for the SPARDL model. The semantics of SPARDL were presented by Event-B and a refinement framework was introduced to develop the Event-B models based on the features of the SPARDL model. Finally, a case study was analyzed to show the effectiveness of our proposed approach to modeling and validation of the SPARDL model by Event-B.

Key words: Space Aircraft Description Language(SPARDL), Event-B, Requirement Analysis, Refinement, Verification

摘要： 针对由周期行为和模式转换机制组成的实时系统提出的SPARDL需求建模语言，详细阐明了其对应的SPARDL模型的Event-B解释。通过Event-B来解释SPARDL的语义，同时提出一种基于SPARDL模型特征的精化框架用于Event-B模型的开发。最后，通过案例研究的分析展示用Event-B对SPARDL模型建模和验证的方法的有效性。

关键词: Space Aircraft Description Language(SPARDL), Event-B, 需求分析, 精化, 验证

QI Yan-xia SHEN Hui-li CHEN Zhao-hui GU Bin. Event-B interpretation for space aircraft description language model[J]. Journal of Computer Applications, 2012, 32(12): 3525-3528.

綦艳霞沈慧丽陈朝晖顾斌. SPARDL模型的Event-B解释[J]. 计算机应用, 2012, 32(12): 3525-3528.

[1]	Xiaonian WU, Jing KUANG, Runlian ZHANG, Lingchen LI. SAT-based impossible differential cryptanalysis of GRANULE cipher [J]. Journal of Computer Applications, 2024, 44(3): 797-804.
[2]	Tao SUN, Zhangtian DUAN, Haonan ZHU, Peihao GUO, Heli SUN. Social event recommendation method based on unexpectedness metric [J]. Journal of Computer Applications, 2024, 44(3): 760-766.
[3]	Chao WANG, Shanshan YAO. Speaker verification method based on speech quality adaptation and triplet-like idea [J]. Journal of Computer Applications, 2024, 44(12): 3899-3906.
[4]	Linhao LI, Xiaoqian ZHANG, Yao DONG, Xu WANG, Yongfeng DONG. Knowledge tracing based on personalized learning and deep refinement [J]. Journal of Computer Applications, 2024, 44(10): 3039-3046.
[5]	Ke FANG, Rong LIU, Chiyu WEI, Xinyue ZHANG, Yang LIU. Pedestrian fall detection algorithm in complex scenes [J]. Journal of Computer Applications, 2023, 43(6): 1811-1817.
[6]	Tao QIU, Jianli DING, Xiufeng XIA, Hongmei XI, Peiliang XIE, Qingyi ZHOU. Efficient complex event matching algorithm based on ordered event lists [J]. Journal of Computer Applications, 2023, 43(2): 423-429.
[7]	Qi WANG, Hang LEI, Xupeng WANG. Deep face verification under pose interference [J]. Journal of Computer Applications, 2023, 43(2): 595-600.
[8]	Yulian ZHANG, Shanshan YAO, Chao WANG, Jiang CHANG. Text-independent speaker verification method based on uncertainty learning [J]. Journal of Computer Applications, 2023, 43(12): 3727-3732.
[9]	LI Kewen, YANG Jiantao, HUANG Zongchao. Improved YOLOv3 target detection based on boundary limit point features [J]. Journal of Computer Applications, 2023, 43(1): 81-87.
[10]	Wei LIU, Cong ZHANG, Wei SHE, Xuan SONG, Zhao TIAN. Data trusted traceability method based on Merkle mountain range [J]. Journal of Computer Applications, 2022, 42(9): 2765-2771.
[11]	Wang TAN, Yi LI. Synthesis of loop bound functions for loop programs [J]. Journal of Computer Applications, 2022, 42(2): 565-573.
[12]	Bin ZHANG, Li WANG, Yanjie YANG. Process tracking multi‑task rumor verification model combined with stance [J]. Journal of Computer Applications, 2022, 42(11): 3371-3378.
[13]	Hexiong CHEN, Yuwei LUO, Yunkai WEI, Wei GUO, Feilu HANG, Zhengxiong MAO, Zhenhong ZHANG, Yingjun HE, Zhenyu LUO, Linjiang XIE, Ning YANG. Blockchain-based data frame security verification mechanism in software defined network [J]. Journal of Computer Applications, 2022, 42(10): 3074-3083.
[14]	WU Kaifan, YIN Xinchun. Lightweight anonymous mutual authentication protocol based on random operators for radio frequency identification system [J]. Journal of Computer Applications, 2021, 41(6): 1621-1630.
[15]	SUN Heli, SUN Yuzhu, ZHANG Xiaoyun. Event description generation based on generative adversarial network [J]. Journal of Computer Applications, 2021, 41(5): 1256-1261.

Event-B interpretation for space aircraft description language model

SPARDL模型的Event-B解释

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics