Extending Timed Abstract State Machines for Real-time Embedded Software

SHAN Jinhui1, ZHANG Lu2,†, WANG Jinbo3, ZHANG Tao3

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; † Corresponding author, E-mail: zhanglu@sei.pku.edu.cn

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

嵌入式系统是用来控制或者监视机器、装置、工厂等大规模设备的系统。嵌入式系统往往有实时性要求: 系统运行结果不仅取决于计算结果是否正确, 还取决于产生结果的时间是否满足要求。作为嵌入式系统的神经中枢, 嵌入式软件有举足轻重的作用。软件需求是关于软件系统的能力、特征或质量因素等的陈述, 这些能力、特征或质量因素是为了让软件系统能对客户有用或有价值[1]。为实时嵌入式软件建立的需求模型可分为3类: 非形式化模型、半形式化模型和形式化模型。早期采用自然语言描述软件需求规格说明。这种非形式化需求模型的优点在于建模成本较低, 缺

点是容易产生歧义, 容易遗漏需求。

半形式化需求模型主要包括数据流图[2]、UML (unified modeling language)图[3]以及其扩展模型MARTE (modeling and analysis of real-time and embedded systems)[4–5]等。MARTE是UML在实时嵌入式领域的扩展, 其优势在于, 图形化需求模型很直观, 易于理解, 缺点是半形式化的需求模型难以支持形式化分析与验证[6]。

形式化需求模型主要包括时间自动机(timed automata, TA)[7]及其扩展模型 Uppaal TA (UTA)[8]、抽象状态机(abstract state machine, ASM)[9]及其扩展模型时间抽象状态机(timed ASM, TASM)[10–13]、Event-b[14–16]、Petri 网[17]、面向航天嵌入式软件的