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

关键词：模型检验 smv 进程阻塞 

单位：61849部队; 广东佛山528248; 武汉大学软件工程国家重点实验室; 湖北武汉430072