PARTIAL ORDER REDUCTION FOR SCALABLE TESTING IN SYSTEM LEVEL DESIGN

• US 20090132991A1
• Filed: 11/05/2008
• Published: 05/21/2009
• Est. Priority Date: 11/16/2007
• Status: Abandoned Application

• Current Assignee: NEC Laboratories America Inc (NEC Corporation)
• Original Assignee: NEC Laboratories America Inc (NEC Corporation)
• Inventors: Kundu, Sudipta, Ganai, Malay K.
• Application Number:
  US12/265,347
• Publication Number:
  US 20090132991A1
• Time in Patent Office: Days
• US Class Current: 716/104
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

A system and method for program testing includes, using a static analysis, determining dependency relations of enabled running processes in a program. The dependency relations are organized in a matrix to provide an interface for exploring the program. A reduced set of possible executions obtained by removal of redundant interleavings as determined with respect to the dependency relation, is explored on the program in a stateless exploration process that analyzes executed states and transitions to verify operation of the program.

Claims

1. A method for concurrent program testing, comprising:

determining dependency relations of running processes in a concurrent program and organizing them in a matrix;

obtaining a reduced set of possible interleavings of processes by removing equivalent interleavings as determined with respect to the dependency relations; and

exploring the reduced set of interleavings to verify operation of the program.

2. The method as recited in claim 1, wherein determining dependency relations includes:

enumerating atomic blocks including sequences of transitions;

obtaining shared variables in each atomic block; and

identifying dependent atomic blocks that represent the dependency relations.

3. The method as recited in claim 1, wherein the dependency relations are obtained statically.

4. The method as recited in claim 1, wherein the dependency relations are obtained dynamically during exploration.

5. The method as in claim 1, wherein the dependency relations are maintained in a query-table, and information is obtained by querying the table during dynamic exploration.

6. The method as recited in claim 1, wherein exploring includes executing an interleaving from the reduced set, and analyzing the reachable states and transitions.

7. The method of claim 6, wherein exploring includes stateless exploration including exploring an interleaving by re-executing the program from its initial state.

8. A computer readable medium comprising a computer readable program, wherein the computer readable program when executed on a computer causes the computer to perform the steps in accordance with claim 1.

9. A system for program testing, comprising:

a static analyzer configured to determine dependency relations of enabled running processes in a program;

a query table configured to organize the dependency relations to provide an interface for exploring the program; and

an explorer engine configured to explore a reduced set of possible interleavings in the program in a stateless exploration process that analyzes executed states and transitions to verify operation of the program.

10. The system as recited in claim 9, wherein the program includes a concurrent program for system level design (SLD) and further comprising:

a parser configured to parse an SLD to generate an intermediate representation of the SLD to be statically analyzed, and

an integration of the explorer engine with a design language specific simulation kernel.

11. The system as recited in claim 9, wherein the query table includes static and dynamic dependency information, and the query table is queried to determine whether running processes need to be interleaved.

12. The system as recited in claim 9, wherein the explorer engine explores an interleaving in the program by re-executing the program from its initial state.

13. The system as recited in claim 9, wherein dependency relations are determined by shared variables between atomic blocks including sequences of transitions and dependent atomic blocks are identified that represent the dependency relations.