基于层次化时间stm软件设计的形式化验证

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