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

摘要

状态迁移矩阵(State Transition Matrix,STM)是一种基于表结构的状态机建模方法,用于建模软件系统行为.但目前STM不具有时间语义,这极大限制了该方法在实时软件建模方面的应用.针对这一问题,本文提出了一种时延STM(Timed STM,TSTM)建模方法,通过为STM各单元格增加时间语义和约束,使之适用于实时软件行为刻画.此外,针对TSTM,给出了一种基于界限模型检测(Bounded Model Checking,BMC)技术的TCTL(Timed Computation Tree Logic)模型检测方法,用以验证TSTM时间及逻辑属性.最后,通过对某型号列控制软件进行TSTM建模与验证,证明上述方法有效性。