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 Jinhui1, ZHANG Lu2,†, WANG Jinbo3, ZHANG Tao3   

  1. 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)


单锦辉1, 张路2,†, 王金波3, 张涛3   

  1. 1. 华为技术有限公司, 深圳 518129
    2. 北京大学信息科学技术学院, 北京 100871
    3. 中国科学院空间应用工程与技术中心, 北京 100094
  • 通讯作者: 张路, E-mail: zhanglu(at)
  • 基金资助:


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为实时嵌入式软件需求建模的有效性。

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