在模型检验工具SMV中实现进程阻塞

模型检验技术是开发高可信软硬件系统的重要途径。目前已经有许多成熟的模型检验工具，SMV就是其中一种常用的工具，可以进行同步或异步系统的自动验证。在异步模型检验中，SMV可以描述进程，但不能直接描述进程的阻塞。本文提出了一种在SMV中利用公平性约束实现阻塞的方法。

To Implement Process Blocking in the Model Checker SMV

Model checking is an important way in developing high confidence software and hardware systems. Nowadays there exist many model checkers, including SMV. SMV can verify systems ranging from completely synchronous to completely asynchronous. In asynchronous system verification, SMV can describe processes, but cannot describe process blocking directly. This paper proposes a method to implement process blocking in SMV with fairness constraint.