Marius Romulus Minea

62091204, Mar 27, 2001

Oct 14, 1998

9/172484

Robert Paul Kurshan - New York NY
Vladimir Levin - New Providence NJ
Marius Minea - Pittsburgh PA
Doron A. Peled - Springfield NJ
Husnu Yenigun - Kucukesat Ankara, TR

Lucent Technologies, Inc. - Murray Hill NJ

G06F17/50

716 5

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.

62955152, Sep 25, 2001

Oct 14, 1998

9/172460

Robert Paul Kurshan - New York NY
Vladimir Levin - New Providence NJ
Marius Minea - Pittsburgh PA
Doron A. Peled - Springfield NJ
Husnu Yenigun - Kucukesat Ankara, TR

Lucent Technologies Inc. - Murray Hill NJ

G06F 760
G06F 1710
G06F 1750
G06G 762

703 13

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.