点击次数：

论文类型：期刊论文

发表时间：2022-06-28

发表刊物：软件学报

所属单位：软件学院

期号：2

页面范围：223-238

ISSN号：1000-9825

摘要：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.

备注：新增回溯数据