model checking,模型检验
我觉得是用以一种符号模拟语言来描述被测设计,以及属性,再通过算法验证。
比如:http://www.cs.technion.ac.il/~ss ... mv/NuSMV.tools.html
NuSMV is a model checker that verifies finite state systems written in a language that is designed to allow the description of such systems, ranging from completely synchronous to completely asynchronous.
It is a reimplementation and extension of SMV, the first model checker based on BDDs.