Extending Timed Abstract State Machines for Real-Time Embedded Software

doi:10.13209/j.0479-8023.2019.005

Acta Scientiarum Naturalium Universitatis Pekinensis ›› 2019, Vol. 55 ›› Issue (2): 197-208.DOI: 10.13209/j.0479-8023.2019.005

Previous Articles Next Articles

Extending Timed Abstract State Machines for Real-Time Embedded Software

SHAN Jinhui¹, ZHANG Lu^2,†, WANG Jinbo³, ZHANG Tao³

1. Huawei Technologies Co. Ltd., Shenzhen 518129
2. School of Electronics Engineering and Computer Science, Peking University, Beijing 100871
3. Technology and Engineering Center for Space Utilization, Chinese Academy of Sciences, Beijing 100094

Received:2018-03-16 Revised:2019-01-09 Online:2019-03-20 Published:2019-03-20
Contact: ZHANG Lu, E-mail: zhanglu(at)sei.pku.edu.cn

实时嵌入式软件时间抽象状态机的扩展

单锦辉¹, 张路^2,†, 王金波³, 张涛³

1. 华为技术有限公司, 深圳 518129
2. 北京大学信息科学技术学院, 北京 100871
3. 中国科学院空间应用工程与技术中心, 北京 100094

通讯作者: 张路, E-mail: zhanglu(at)sei.pku.edu.cn
基金资助:
国家自然科学基金(61225007)资助

Abstract

Abstract:

According to the deficiency of Timed Abstract State Machine (TASM), TASM is extended with the data type of arrays, a loop rule named “while”, and some operators such as “%”,“&”, “|”, “^”, “>>”, “<<”, etc. The syntax and semantics of the extended TASM are defined. The extended TASM is applied to actual real-time embedded software to validate its effectiveness for requirements modeling.

Key words: requirements modeling language, real-time, embedded software, formal definition, extension, timed abstract state machine

摘要：

针对时间抽象状态机(TASM)存在的不足, 对TASM进行扩展, 增加数组数据类型、while循环处理规则以及“%”, “&”, “|”, “^”, “>>”和“<<”等运算符, 定义扩展后TASM的语法和语义。采用扩展后的TASM为实际的实时嵌入式软件需求建模, 通过实验, 验证了采用扩展后的TASM为实时嵌入式软件需求建模的有效性。

关键词: 需求建模语言, 实时, 嵌入式软件, 形式化定义, 扩展, 时间抽象状态机

SHAN Jinhui, ZHANG Lu, WANG Jinbo, ZHANG Tao. Extending Timed Abstract State Machines for Real-Time Embedded Software[J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2019, 55(2): 197-208.

单锦辉, 张路, 王金波, 张涛. 实时嵌入式软件时间抽象状态机的扩展[J]. 北京大学学报自然科学版, 2019, 55(2): 197-208.

Add to citation manager EndNote|Ris|BibTeX

URL: https://xbna.pku.edu.cn/EN/10.13209/j.0479-8023.2019.005

https://xbna.pku.edu.cn/EN/Y2019/V55/I2/197

[1]	WANG Fanlin, HE Xinqiang, WANG Donghui. Research and Development of Living Plants in-vivo Fluorescence Imaging System for Experimental Teaching [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2024, 60(1): 127-132.
[2]	ZHAO Xiujia, LI Lei, LIU Xianhua. Instruction Extension Ensuring Time Constraints in Real Time Processor [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2023, 59(2): 179-188.
[3]	WANG Qi, TANG Jianzhou, CHENG Jian, DUAN Tiejun, DING Cong, ZHANG Huaihui, MENG Yunxi, ZHANG Zhicheng. Geochronological and Geochemical Characteristics of the Middle Permian Rhyolite and Its Geological Implications in Siziwang Banner, Inner Mongolia [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2022, 58(3): 453-468.
[4]	QU Yonglin, WEN Xinyu, ZHANG Muqi, LIU Zhe. Develop an Objective Post-processing System with Artificial Neural Network to Improve Numerical Weather Prediction for the Olympic Winter Games Beijing 2022 [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2022, 58(2): 210-220.
[5]	ZHANG Yang, XIAN Huiting, ZHAO Zhijie. Real-Time River Water Quality Prediction Model Based on Spatial Correlation and Neural Network Model [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2022, 58(2): 337-344.
[6]	YANG Xingwen, YONG Shanshan, WANG Xin’an, ZHOU Kangsheng, JIN Xiuru. Design and Implementation of Data Acquisition System for AETA [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2020, 56(4): 600-606.
[7]	BAO Yingyu, XIE Hui, CHEN Lüjun, WEN Donghui. Variations of 4 Antibiotic Resistance Genes in a Sewage Treatment Plant [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2020, 56(4): 772-776.
[8]	WANG Wenchao, Lü Xueqiang, ZHANG Kai, ZHOU Jianshe. Research on Automatic Writing of Football Game News [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2018, 54(2): 271-278.
[9]	LIU Chao, YAN Wei. High-Speed Hardware Design of Kalman Filter Based on FPU with Formula Derivation Method [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2016, 52(5): 803-808.
[10]	LI Jianbo, GUO Lei, OUYANG Zhixia, ZENG Tao, DING Yuanjun, ZHANG Ying. Strain and Kinematic Vorticity Analysis of the Liaonan Metamorphic Core Complex Ductile Detachment Zone [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2015, 51(6): 1078-1090.
[11]	CHEN Yan,ZHANG Zhicheng,LI Ke,LUO Zhiwen,TANG Wenhao,LI Qiugen. Geochronology, Geochemistry and Geological Significance of the Permian Bimodal Volcanic Rocks in Xi Ujimqin Banner, Inner Mongolia [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2014, 50(5): 843-858.
[12]	WANG Teng,WANG Xin’an,XIE Zheng,HU Ziyi. Low-Cost VLSI Implementation of Motion Estimation for H.264/AVC Encoders [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2014, 50(4): 768-780.
[13]	YANG Shengbin,LIU Zhongbao,GENG Xinxia. Relationship Between Gas Accumulation and Structural Characteristics of Extensional-Shear Fault System in Yakela Fault Block [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2013, 49(2): 269-276.
[14]	SUN Haimei,SUN Weiling,SHAO Jun. Quantifying Total Bacteria and Functional Genes of Denitrifying Bacteria in Buji River in Dry Season [J]. Acta Scientiarum Naturalium Universitatis Pekinensis, 2012, 48(4): 629-638.
[15]	SHU Wulin,HOU Guiting,WANG Chuancheng,XIAO Fangfeng,LI Le. Geochemistry and Geological Implications of Mafic Dyke Swarms in the Southwestern Area of Zhongtiao Mountains [J]. , 2011, 47(6): 1055-1062.

Extending Timed Abstract State Machines for Real-Time Embedded Software

实时嵌入式软件时间抽象状态机的扩展

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics