Software Formal Modeling and Verification Method Based on Time STM
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 01,2014
  • Revised:October 31,2014
  • Adopted:
  • Online: February 06,2015
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063