J4 ›› 2006, Vol. 28 ›› Issue (3): 85-87.
• 论文 • 上一篇 下一篇
王常春[1] 董威[2]
出版日期:
发布日期:
Online:
Published:
摘要：
模型检验技术是开发高可信软硬件系统的重要途径。目前已经有许多成熟的模型检验工具，SMV就是其中一种常用的工具，可以进行同步或异步系统的自动验证。在异步模型检验中，SMV可以描述进程，但不能直接描述进程的阻塞。本文提出了一种在SMV中利用公平性约束实现阻塞的方法。
关键词: 模型检验 SMV 进程阻塞
Abstract:
Model checking is an important way in developing high confidence software and hardware systems. Nowadays there exist many model checkers, including SM 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.
Key words: model checking ;SMV, process blocking
王常春[1] 董威[2]. 在模型检验工具SMV中实现进程阻塞[J]. J4, 2006, 28(3): 85-87.
0 / / 推荐
导出引用管理器 EndNote|Ris|BibTeX
链接本文: http://joces.nudt.edu.cn/CN/
http://joces.nudt.edu.cn/CN/Y2006/V28/I3/85
