点击次数：

论文类型：期刊论文

发表时间：2014-08-15

发表刊物：计算机科学

收录刊物：PKU、ISTIC、CSCD

卷号：41

期号：8

页面范围：42-46

ISSN号：1002-137X

关键字：层次化时间状态迁移矩阵;形式化验证;有界模型检测

摘要：状态迁移矩阵(State Transition Matrix,STM)是一种基于表结构的程序建模语言.事件变量类型单一,事件和状态数量的增加很容易造成状态空间爆炸问题,无法表达具有时间语义的软件系统等原因,极大限制了该建模方法的推广应用.文中针对这些问题,首先提出层次化时间状态迁移矩阵(Hierarchical Time State Transition Matrix,HTSTM)模型,用于设计、建模和验证具有时间条件约束的软件系统,并给出形式化表示方法.基于该表示方法提出一种符号化编码方法,采用有界模型检测思想将需要验证的LTL性质输入SMT(Satisfiability Modulo Theories)求解器进行验证,从而在一定程度上证明了软件设计的正确性.