主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
侯刚,周宽久,常军旺,王洁,李明楚.基于时间STM的软件形式化建模与验证方法.软件学报,2015,26(2):223-238
基于时间STM的软件形式化建模与验证方法
Software Formal Modeling and Verification Method Based on Time STM
投稿时间:2014-07-01  修订日期:2014-10-31
DOI:10.13328/j.cnki.jos.004777
中文关键词:  时间STM  界限模型检测  时间计算树逻辑  实时嵌入式软件
英文关键词:time STM  bounded model checking  time computation tree logic  real-time embedded software
基金项目:国家自然科学基金(61402073, 61272174)
作者单位E-mail
侯刚 大连理工大学 软件学院, 辽宁 大连 116623  
周宽久 大连理工大学 软件学院, 辽宁 大连 116623  
常军旺 大连理工大学 软件学院, 辽宁 大连 116623  
王洁 大连理工大学 软件学院, 辽宁 大连 116623 wangjie1003@163.com 
李明楚 大连理工大学 软件学院, 辽宁 大连 116623  
摘要点击次数: 3377
全文下载次数: 2775
中文摘要:
      状态迁移矩阵(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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利