###
Journal of Software:2015.26(2):223-238

基于时间STM的软件形式化建模与验证方法
侯刚,周宽久,常军旺,王洁,李明楚
(大连理工大学 软件学院, 辽宁 大连 116623)
Software Formal Modeling and Verification Method Based on Time STM
HOU Gang,ZHOU Kuan-Jiu,CHANG Jun-Wang,WANG Jie,LI Ming-Chu
(School of Software Technology, Dalian University of Technology, Dalian 116623, China)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 4205   Download 2994
Received:July 01, 2014    Revised:October 31, 2014
> 中文摘要: 状态迁移矩阵(state transition matrix,简称STM)是一种基于表结构的状态机建模方法,前端为表格形式,后端则具有严格的形式化定义,用于建模软件系统行为.但目前STM不具有时间语义,这极大地限制了该方法在实时嵌入式软件建模方面的应用.针对这一问题,提出了一种基于时间STM(time STM,简称TSTM)的形式化建模方法,通过为STM各单元格增加时间语义和约束,使其适用于实时软件行为刻画.此外,针对TSTM给出了一种基于界限模型检测(bounded model checking,简称BMC)技术的时间计算树逻辑(time computation tree logic,简称TCTL)模型检测方法,以验证TSTM时间及逻辑属性.最后,通过对某型号列控制软件进行TSTM建模与验证,证明了上述方法的有效性.
Abstract: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.
文章编号:     中图分类号:    文献标志码:
基金项目:国家自然科学基金(61402073, 61272174) 国家自然科学基金(61402073, 61272174)
Foundation items:
Reference text:

侯刚,周宽久,常军旺,王洁,李明楚.基于时间STM的软件形式化建模与验证方法.软件学报,2015,26(2):223-238

HOU Gang,ZHOU Kuan-Jiu,CHANG Jun-Wang,WANG Jie,LI Ming-Chu.Software Formal Modeling and Verification Method Based on Time STM.Journal of Software,2015,26(2):223-238