点击次数：

论文类型：期刊论文

发表时间：2015-02-15

发表刊物：软件学报

收录刊物：EI、PKU、ISTIC、CSCD、Scopus

卷号：26

期号：2

页面范围：223-238

ISSN号：1000-9825

关键字：时间STM;界限模型检测;时间计算树逻辑;实时嵌入式软件

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