Hits:

Indexed by:期刊论文

Date of Publication:2015-02-15

Journal:软件学报

Included Journals:EI、PKU、ISTIC、CSCD、Scopus

Volume:26

Issue:2

Page Number:223-238

ISSN No.:1000-9825

Key Words:时间STM;界限模型检测;时间计算树逻辑;实时嵌入式软件

Abstract:状态迁移矩阵(state transition matrix,简称STM)是一种基于表结构的状态机建模方法,前端为表格形式,后端则具有严格的形式化定义,用于建模软件系统行为。但目前 STM 不具有时间语义,这极大地限制了该方法在实时嵌入式软件建模方面的应用。针对这一问题,提出了一种基于时间STM(time STM,简称TSTM)的形式化建模方法,通过为STM各单元格增加时间语义和约束,使其适用于实时软件行为刻画。此外,针对TSTM给出了一种基于界限模型检测(bounded model checking,简称BMC)技术的时间计算树逻辑(time computation tree logic,简称TCTL)模型检测方法,以验证 TSTM 时间及逻辑属性。最后,通过对某型号列控制软件进行 TSTM 建模与验证,证明了上述方法的有效性。