基于时延STM的软件形化建模与验证方法
状态迁移矩阵(State Transition Matrix,STM)是一种基于表结构的状态机建模方法,用于建模软件系统行为.但目前STM不具有时间语义,这极大限制了该方法在实时软件建模方面的应用.针对这一问题,本文提出了一种时延STM(Timed STM,TSTM)建模方法,通过为STM各单元格增加时间语义和约束,使之适用于实时软件行为刻画.此外,针对TSTM,给出了一种基于界限模型检测(Bounded Model Checking,BMC)技术的TCTL(Timed Computation Tree Logic)模型检测方法,用以验证TSTM时间及逻辑属性.最后,通过对某型号列控制软件进行TSTM建模与验证,证明上述方法有效性。
计算机软件 形化建模 验证技术 时延状态迁移矩阵
侯刚 周宽久 王洁 常军旺 李明楚
大连理工大学软件学院,大连116620
国内会议
长沙
中文
156-165
2014-10-16（万方平台首次上网日期，不代表论文的发表时间）