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

摘要

状态迁移矩阵(state transition matrix,简称STM)是一种基于表结构的状态机建模方法,前端为表格形式,后端则具有严格的形式化定义,用于建模软件系统行为。但目前 STM 不具有时间语义,这极大地限制了该方法在实时嵌入式软件建模方面的应用。针对这一问题,提出了一种基于时间STM(time STM,简称TSTM)的形式化建模方法,通过为STM各单元格增加时间语义和约束,使其适用于实时软件行为刻画。此外,针对TSTM给出了一种基于界限模型检测(bounded model checking,简称BMC)技术的时间计算树逻辑(time computation tree logic,简称TCTL)模型检测方法,以验证 TSTM 时间及逻辑属性。最后,通过对某型号列控制软件进行 TSTM 建模与验证,证明了上述方法的有效性。%State transition matrix (STM), designed for modeling software system, is a table-based modeling language in which the front-end is expressed in the table form and the back-end has strict formalized definition. At present, however, STM has no time semantics, which greatly limits the application of this method in real-time embedded software modeling. In order to solve this problem, this paper proposes a time STM (TSTM) modeling method attained by adding time semantics and constraint for each cell in STM, making it suitable for describing real-time system behavior. In addition, a time computation tree logic (TCTL) model checking method is presented based on bounded model checking (BMC) technology for verification of time and logic properties of TSTM model. At last, the effectiveness of the proposed method is validated by modeling and verifying certain type train control software.