|
个人信息Personal Information
教授
博士生导师
硕士生导师
主要任职：Director of Academic Committee at Kaifa District
其他任职：开发区校区学术分委员会主任（Director of Academic Committee at Kaifa Campus）
性别：男
毕业院校：多伦多大学
学位：博士
所在单位：软件学院、国际信息与软件学院
学科：软件工程. 运筹学与控制论
办公地点：开发区（Kaifa District Campus）
联系方式：mingchul@dlut.edu.cn
电子邮箱：mingchul@dlut.edu.cn
扫描关注
基于时延STM的软件形化建模与验证方法
点击次数：
论文类型：会议论文
发表时间：2014-10-16
页面范围：156-165
关键字：计算机软件;形化建模;验证技术;时延状态迁移矩阵
摘要：状态迁移矩阵(State Transition Matrix,STM)是一种基于表结构的状态机建模方法,用于建模软件系统行为.但目前STM不具有时间语义,这极大限制了该方法在实时软件建模方面的应用.针对这一问题,本文提出了一种时延STM(Timed STM,TSTM)建模方法,通过为STM各单元格增加时间语义和约束,使之适用于实时软件行为刻画.此外,针对TSTM,给出了一种基于界限模型检测(Bounded Model Checking,BMC)技术的TCTL(Timed Computation Tree Logic)模型检测方法,用以验证TSTM时间及逻辑属性.最后,通过对某型号列控制软件进行TSTM建模与验证,证明上述方法有效性。