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

Modeling and Formal Verification for Software Designs Based on Hierarchical Timed State Transition Matrix

作　　者：周宽久[1,2] 任龙涛[1] 王小龙[1] 勇嘉伟[1] 侯刚[1] 

机构地区：[1]大连理工大学软件学院,大连116620 [2]大连理工大学软件评测中心,大连116620

出　　处：《计算机科学》2014年第8期42-46,共5页Computer Science

基　　金：国家自然科学基金(61272174)资助

摘　　要：状态迁移矩阵(State Transition Matrix,STM)是一种基于表结构的程序建模语言。事件变量类型单一,事件和状态数量的增加很容易造成状态空间爆炸问题,无法表达具有时间语义的软件系统等原因,极大限制了该建模方法的推广应用。文中针对这些问题,首先提出层次化时间状态迁移矩阵(Hierarchical Time State Transition Matrix,HTSTM)模型,用于设计、建模和验证具有时间条件约束的软件系统,并给出形式化表示方法。基于该表示方法提出一种符号化编码方法,采用有界模型检测思想将需要验证的LTL性质输入SMT(Satisfiability Modulo Theories)求解器进行验证,从而在一定程度上证明了软件设计的正确性。State Transition Matrix （STM） is a table-based modeling language. The popularization and application of this modeling method are greatly limited by the singleness of its event variable type, the state space explosion problem caused by the increasing events and states, and the weak expressive power in time semantics of software systems. We firstly presented a concept of Hierarchical Timed State Transition Matrix （HTSTM） which is mainly used for design, modeling and verification of software systems with time constraints. Then a formalization of HTSTM designs was pro- vided as a state transition system. Based on the formalization,we proposed a symbolic encoding approach which adopts the idea of Bounded Model Checking （BMC）. Finally the LTL properties to be verified were determined by Satisfiability Modulo Theories （SMT） so that the correctness of the software design was proved to a certain extent.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]