符号模型判别系统的一种实用反例生成策略被引量：1

下载PDF

导出

摘要描述一个在模型判别器中实现的实用的反例生成策略。该策略利用电路性质描述语言的特点 ,将所有的“反例”生成算法归结为三种基本的“正例”生成算法。

作者范轶平贝劲松边计年薛宏熙洪先龙

机构地区清华大学计算机系设计自动化教研组

出处《计算机应用》 CSCD 2000年第S1期165-167,170,共4页 journal of Computer Applications

基金国家关键基础研究和发展计划!(973) (G1 9980 30 4 1 1 )

关键词形式验证模型判别反例生成 CTL

参考文献9

1E. M. Clarke,O. Grumberg,K. L. McMillan,et al.Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking[].nd Design Automatic Conference.1995
2J. R. Burch,E. M. Clarke,D. E. Long.Symbolic model checking with partitioned transition relations[C].Proc International Conference of VLSI Aug.1991
3E. M. Clarke,E. A. Emerson,A. P. Sistla.Automatic verification of finite - state concurrent systems using temporal logic specifications[].ACM Transactions on Programming Languages and Systems.1986
4J. R. Burch,E. M. Clarke,D. E. Long,et al.Symbolic model checking for sequential circuit verification[].In IEEE Trans On Computer-Aided Design of Integrated Circuits and Systems.1994
5O. Caudate,C. Berthed,J. C. Madder.Verification of sequential machines using functional vectors[].International Workshop on Applied Formal Methods for Correct VLSI Design volume VLSI Design Methods-II.1990
6VHDL:HardwareDescriptionandDesign. . 1 989
7K.L.McMillan.SymbolicModelChecking:AnApproachtotheStateExplosionProblem. . 1 992
8K.L.McMillan.TheSMVSystem. . 1 992
9R.K.Brayton,,E.M.Clarke,P.A.Subrahmanyam.FormalMethodsinSystemDesign[]..1995

计算机应用

2000年第S1期

内容加载中请稍等...