基于时间STM的软件形式化建模与验证方法

来源：软件学报杂志2015年第2期北京时间：

作者：侯刚,周宽久,常军旺,王洁,李明楚

单位：侯刚，大连理工大学 软件学院, 辽宁 大连 11662311,周宽久，大连理工大学 软件学院, 辽宁 大连 11662302,常军旺，大连理工大学 软件学院, 辽宁 大连 11662303,王洁，大连理工大学 软件学院, 辽宁 大连 11662304,李明楚，大连理工大学 软件学院, 辽宁 大连 11662305

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

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

基金资助：国家自然科学基金(61402073, 61272174)