计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2014年
8期
42-46
,共5页
周宽久%任龙涛%王小龙%勇嘉伟%侯刚
週寬久%任龍濤%王小龍%勇嘉偉%侯剛
주관구%임룡도%왕소룡%용가위%후강
层次化时间状态迁移矩阵%形式化验证%有界模型检测
層次化時間狀態遷移矩陣%形式化驗證%有界模型檢測
층차화시간상태천이구진%형식화험증%유계모형검측
Hierarchical time state transition matrix%Formal verification%Bounded model checking
状态迁移矩阵(State Transition Matrix,STM)是一种基于表结构的程序建模语言.事件变量类型单一,事件和状态数量的增加很容易造成状态空间爆炸问题,无法表达具有时间语义的软件系统等原因,极大限制了该建模方法的推广应用.文中针对这些问题,首先提出层次化时间状态迁移矩阵(Hierarchical Time State Transition Matrix,HTSTM)模型,用于设计、建模和验证具有时间条件约束的软件系统,并给出形式化表示方法.基于该表示方法提出一种符号化编码方法,采用有界模型检测思想将需要验证的LTL性质输入SMT(Satisfiability Modulo Theories)求解器进行验证,从而在一定程度上证明了软件设计的正确性.
狀態遷移矩陣(State Transition Matrix,STM)是一種基于錶結構的程序建模語言.事件變量類型單一,事件和狀態數量的增加很容易造成狀態空間爆炸問題,無法錶達具有時間語義的軟件繫統等原因,極大限製瞭該建模方法的推廣應用.文中針對這些問題,首先提齣層次化時間狀態遷移矩陣(Hierarchical Time State Transition Matrix,HTSTM)模型,用于設計、建模和驗證具有時間條件約束的軟件繫統,併給齣形式化錶示方法.基于該錶示方法提齣一種符號化編碼方法,採用有界模型檢測思想將需要驗證的LTL性質輸入SMT(Satisfiability Modulo Theories)求解器進行驗證,從而在一定程度上證明瞭軟件設計的正確性.
상태천이구진(State Transition Matrix,STM)시일충기우표결구적정서건모어언.사건변량류형단일,사건화상태수량적증가흔용역조성상태공간폭작문제,무법표체구유시간어의적연건계통등원인,겁대한제료해건모방법적추엄응용.문중침대저사문제,수선제출층차화시간상태천이구진(Hierarchical Time State Transition Matrix,HTSTM)모형,용우설계、건모화험증구유시간조건약속적연건계통,병급출형식화표시방법.기우해표시방법제출일충부호화편마방법,채용유계모형검측사상장수요험증적LTL성질수입SMT(Satisfiability Modulo Theories)구해기진행험증,종이재일정정도상증명료연건설계적정학성.
