Incremental CTL Model Checker for Fair States

スポンサーリンク

概要

• 論文の詳細を見る

• CTL (Computation Tree Logic) model checking is a formal method for design verification that checks whether the behavior of the verified system is contained in that of the requirements specification. If this check doesn't, pass, the CTL model checker generates a subset of fair states which belongs to the system but not to the specification. In this letter, we present an incremental method which successively modifies the latest verification result each time the design is modified. Our incremental algorithm allows the designer to make changes in terms of addition or subtraction of fair CTL formulas, or fairness constraints on acceptable behavior from the problem statement. Then, these changes are adopted to update the set of fair states computed earlier. Our incremental algorithm is shown to be better than the current non-incremental techniques for CTL model checking. Furthermore, a conclusion supported by the experimental results is presented herein.

• 社団法人電子情報通信学会の論文
• 1999-07-25

著者

• Shen Victor

  Department Of Electrical Engineering Mingchi Institute Of Technology

関連論文

• Incremental CTL Model Checker for Fair States
• A Novel Cryptosystem with Lock Generation and Sum-Difference Replacement Ladder

スポンサーリンク