公开(公告)号：US20060248515A1

公开(公告)日：2006-11-02

申请号：US11119530

申请日：2005-04-29

申请人： Shaz Qadeer ,  Sriram Rajamani ,  Vladimir Levin ,  Robert Palmer

发明人： Shaz Qadeer ,  Sriram Rajamani ,  Vladimir Levin ,  Robert Palmer

IPC分类号： G06F9/44

CPC分类号： G06F8/433 ,  G06F8/456 ,  G06F11/3608

摘要： Described techniques and tools help model checking scale to large programs while reducing missed errors. In particular, described techniques and tools help reduce the state space of concurrent programs without depending on cycle detection and without scheduling execution of postponed threads at all cycles. For example, described techniques and tools use a type of partial-order reduction called transaction-based reduction to reduce program state space. Analysis is performed at commit points to determine whether to schedule delayed threads.

摘要翻译： 描述的技术和工具可帮助模型检查大型程序的规模，同时减少错误的错误。 特别地，所描述的技术和工具有助于减少并发程序的状态空间，而不依赖于周期检测，并且不调度在所有周期执行延迟的线程。 例如，所描述的技术和工具使用一种称为基于事务的减少的部分顺序减少来减少程序状态空间。 分析在提交点执行，以确定是否计划延迟的线程。

公开(公告)号：US06209120B1

公开(公告)日：2001-03-27

申请号：US09172484

申请日：1998-10-14

申请人： Robert Paul Kurshan ,  Vladimir Levin ,  Marius Minea ,  Doron A. Peled ,  Husnu Yenigun

发明人： Robert Paul Kurshan ,  Vladimir Levin ,  Marius Minea ,  Doron A. Peled ,  Husnu Yenigun

IPC分类号： G06F1750

CPC分类号： G06F11/3604 ,  G06F17/504

摘要： A method and apparatus that employs static partial order reduction and symbolic verification allow the design of a system that includes both hardware and software to be verified. The system is specified in a hardware-centric language and a software-centric language, as appropriate, and properties are verified one at a time. Each property is identified whether it is hardware-centric or software-centric. A hardware-centric property that contains little software is does not employ the static partial order reduction. Software-centric properties, and hardware-centric properties that have substantial amounts of software do employ the static partial order reduction. Following partial order reduction, the software-centric language specifications are converted to synchronous form and combined with the hardware-centric specifications. The combined specification is applied to a symbolic verification tool, such as COSPAN, and the results are displayed.

摘要翻译： 采用静态部分顺序减少和符号验证的方法和装置允许包括硬件和软件两者的系统的设计被验证。 系统以硬件为中心的语言和以软件为中心的语言进行指定，并且属性一次验证。 确定每个属性是以硬件为中心还是以软件为中心。 包含很少软件的以硬件为中心的属性不采用静态部分顺序缩减。 以软件为中心的属性以及具有大量软件的以硬件为中心的属性都采用静态部分顺序降级。 在部分降序后，以软件为中心的语言规范转换为同步格式，并结合以硬件为中心的规范。 组合规格应用于符号验证工具（如COSPAN），并显示结果。

公开(公告)号：US06295515B1

公开(公告)日：2001-09-25

申请号：US09172460

申请日：1998-10-14

申请人： Robert Paul Kurshan ,  Vladimir Levin ,  Marius Minea ,  Doron A. Peled ,  Husnu Yenigun

发明人： Robert Paul Kurshan ,  Vladimir Levin ,  Marius Minea ,  Doron A. Peled ,  Husnu Yenigun

IPC分类号： G06F760

CPC分类号： G06F11/3608 ,  G06F17/504

摘要： A static partial order reduction generator and process result in a substantially reduced state space graph of a multi-process system, independently of the model checking process. The process of this invention creates a modified state graph generator with appended rules that allow any desired state searching tactic (breadth first, depth first, etc.) to be employed when states and transitions are considered in the course of verification. This permits use of existing model checking tools without needing to modify them. The static partial order reduction is made possible by realizing that a prior art condition that at least one state along each cycle of the reduced state graph must be fully expanded can be guaranteed by considering the individual processes that make up the system and identifying certain transitions in those processes.

摘要翻译： 静态部分降序生成器和过程导致多进程系统的基本上减小的状态空间图，与模型检查过程无关。 本发明的过程创建具有附加规则的修改的状态图生成器，其允许在验证过程中考虑状态和转换时使用任何期望的状态搜索策略（宽度优先，深度优先等）。 这允许使用现有的模型检查工具，而不需要修改它们。 通过认识到现有技术的条件是，通过考虑构成系统的各个过程并且识别某些转换，可以保证沿着缩小状态图的每个周期的至少一个状态必须被完全扩展的现有技术条件 这些过程。