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]	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.
[2]	SUN Heli, SUN Yuzhu, ZHANG Xiaoyun. Event description generation based on generative adversarial network [J]. Journal of Computer Applications, 2021, 41(5): 1256-1261.
[3]	BAO Yulong, ZHU Xueyang, ZHANG Wenhui, SUN Pengfei, ZHAO Yingqi. Formal verification of smart contract for access control in IoT applications [J]. Journal of Computer Applications, 2021, 41(4): 930-938.
[4]	LI Xiuyan, LIU Mingxi, SHI Wenbo, DONG Guofang. Efficient dynamic data audit scheme for resource-constrained users [J]. Journal of Computer Applications, 2021, 41(2): 422-432.
[5]	SUN Heli, XU Tong, HE Liang, JIA Xiaolin. Personalized social event recommendation method integrating user historical behaviors and social relationships [J]. Journal of Computer Applications, 2021, 41(2): 324-329.
[6]	CHEN Zhen, ZHONG Yiwen, LIN Juan. Hybrid greedy genetic algorithm for solving 0-1 knapsack problem [J]. Journal of Computer Applications, 2021, 41(1): 87-94.
[7]	ZHANG Linghao, WANG Sheng, ZHOU Hui, CHEN Yifan, GUI Shenglin. Secure communication scheme of unmanned aerial vehicle system based on MAVLink protocol [J]. Journal of Computer Applications, 2020, 40(8): 2286-2292.
[8]	PAN Guoteng, OU Guodong, CHAO Zhanghu, LI Mengjun. Design and implementation of Lite register model [J]. Journal of Computer Applications, 2020, 40(5): 1369-1373.
[9]	SHAN Xiaohuan, ZHANG Zhiguo, SONG Baoyan, REN Chenglin. Activity recommendation method based on directed label graph and user feedback in event-based social network [J]. Journal of Computer Applications, 2020, 40(2): 448-453.
[10]	QIN Biao, GUO Fan, TU Fengtao. Correctness verification of static taint analysis results for Android application [J]. Journal of Computer Applications, 2019, 39(10): 3018-3027.
[11]	SHEN Minjie, ZENG Zhenbing, LIN Wang, YANG Zhengfeng. Safety verification of stochastic continuous system using stochastic barrier certificates [J]. Journal of Computer Applications, 2018, 38(6): 1737-1744.
[12]	XU Mingdi, GAO Yang, GAO Xueyuan, ZHANG Fan. Correspondence property-based platform configuration attestation [J]. Journal of Computer Applications, 2018, 38(2): 337-342.
[13]	JIA Shangkun, HE Fei. Software regression verification based on witness automata [J]. Journal of Computer Applications, 2018, 38(10): 2990-2995.
[14]	XU Xin, LIANG Jiuzhen. Unconstrained face verification based on 3D frontalization and similarity learning [J]. Journal of Computer Applications, 2018, 38(10): 2788-2793.
[15]	LI Sai, LI Xiaoyu. Mobile secure payment solution based on encrypted SMS verification code [J]. Journal of Computer Applications, 2017, 37(8): 2270-2274.

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