%0 Journal Article
%T 基于层次化时间stm软件设计的形式化验证
%A 周宽久？
%A 任龙涛？
%A 王小龙？
%A 勇嘉伟？
%A 侯刚？
%J 计算机科学
%D 2014
%R 10.11896/j.issn.1002-137X.2014.08.008
%X 状态迁移矩阵(statetransitionmatrix,stm)是一种基于表结构的程序建模语言。事件变量类型单一,事件和状态数量的增加很容易造成状态空间爆炸问题,无法表达具有时间语义的软件系统等原因,极大限制了该建模方法的推广应用。文中针对这些问题,首先提出层次化时间状态迁移矩阵(hierarchicaltimestatetransitionmatrix,htstm)模型,用于设计、建模和验证具有时间条件约束的软件系统,并给出形式化表示方法。基于该表示方法提出一种符号化编码方法,采用有界模型检测思想将需要验证的ltl性质输入smt(satisfiabilitymodulotheories)求解器进行验证,从而在一定程度上证明了软件设计的正确性。
%K 层次化时间状态迁移矩阵
%K 形式化验证
%K 有界模型检测
%U http://www.jsjkx.com/jsjkx/ch/reader/view_abstract.aspx?file_no=20140808&flag=1