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

Extending Timed Abstract State Machines for Real-Time Embedded Software

作　　者：单锦辉 张路[2] 王金波[3] 张涛[3] SHAN Jinhui;ZHANG Lu;WANG Jinbo;ZHANG Tao(Huawei Technologies Co. Ltd., Shenzhen 518129;School of Electronics Engineering and Computer Science,Peking University, Beijing 100871;Technology and Engineering Center for Space Utilization, Chinese Academyof Sciences, Beijing 100094)

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

出　　处：《北京大学学报（自然科学版）》2019年第2期197-208,共12页Acta Scientiarum Naturalium Universitatis Pekinensis

基　　金：国家自然科学基金(61225007)资助

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

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]