PARALLELIZING BOUNDED MODEL CHECKING USING TUNNELS OVER A DISTRIBUTED FRAMEWORK

• US 20100011057A1
• Filed: 09/24/2008
• Published: 01/14/2010
• Est. Priority Date: 07/14/2008
• Status: Active Grant

• Current Assignee: NEC Corporation
• Original Assignee: NEC Laboratories America Inc (NEC Corporation)
• Inventors: GANAI, MALAY
• Granted Patent: US 8,504,330 B2
• Time in Patent Office: Days
• US Class Current: 709/203
• CPC Class Codes: G06F 9/5066 Algorithms for mapping a plurality of inter-dependent sub-tasks onto a plurality of physical CPUs mappping at compile time, see G06F8/451

Abstract

A system and method for bounded model checking of computer programs includes decomposing a program having at least one reachable property node for bounded model checking (BMC) into sub-problems by employing a tunneling and slicing-based (TSR) BMC reduction method. The sub-problems of the TSR method are partitioned in a distributed environment, where the distributed environment includes at least one master processing unit and at least one client unit. The sub-problems are solved by each client independently of other clients to reduce communication overhead and provide scalability.

Claims

1. A method for bounded model checking of computer programs, comprising:

decomposing a program having at least one reachable property node for bounded model checking (BMC) into sub-problems by employing a tunneling and slicing-based (TSR) BMC reduction method by;

assigning the sub-problems of the TSR method in a distributed environment, where the distributed environment includes at least one master processing unit and at least one client unit; and

solving the sub-problems by each client independently of other clients to reduce communication overhead and provide scalability.

2. The method as recited in claim 1, wherein decomposing includes:

creating at least one tunnel based on disjunctive control paths through the program;

obtaining a reduced EMC sub-problem using BMC unrolling, while using path constraints imposed by the at least one tunnel; and

for the reachable property node, determining a quantifier-free formula (QFP) in a decidable subset of first order logic; and

checking satisfiability of the QFP, independently and individually, to determine whether the QFP is satisfiable for the sub-problem.

3. The method as recited in claim 1, further comprising continuing the decomposing until a BMC bound is reached.

4. The method as recited in claim 1, wherein the at least one master controls activity of the at least one client and the method further comprises dynamically adjusting an available pool of clients based on client responses.

5. The method as recited in claim 4, wherein dynamically adjusting includes removing clients that do not respond in accordance with a synchronization schedule and adding these clients back when these clients tender a response.

6. The method as recited in claim 1, wherein the at least one master and the at least one client are arranged for communication such that the clients communicate only with the at least one master.

7. The method as recited in claim 1, further comprising disjunctive partitioning wherein independent sub-problems are created deterministically by clients, and solving includes statically solving an exclusive subset of sub-problems by clients.

8. The method as recited in claim 1, further comprising assigning a sub-problem by notifying a client of a partition identifier and a corresponding BMC depth.

9. A method for bounded model checking of computer programs, comprising:

decomposing a program having at least one reachable property node for bounded model checking (BMC) into sub-problems by employing a tunneling and slicing-based (TSR) BMC reduction method by;

assigning sub-problems by a master controller to one or more clients controllers;

partitioning the sub-problems of the TSR method by a client controller or the master controller in response to a first message from the master controller; and

solving the sub-problems by a respective client corresponding to a second message from the master controller, where solving is performed independently of other clients to reduce communication overhead and provide scalability.

10. The method as recited in claim 9, wherein decomposing includes:

creating at least one tunnel based on disjunctive control paths through the program;

obtaining a reduced BMC sub-problem using BMC unrolling, while using path constraints imposed by the at least one tunnel; and

for the reachable property node, determining a quantifier-free formula (QFP) in a decidable subset of first order logic; and

checking satisfiability of the QFP, independently and individually, to determine whether the QFP is satisfiable for the sub-problem.

11. The method as recited in claim 9, further comprising continuing the decomposing until a BMC bound is reached.

12. The method as recited in claim 9, wherein the master controller controls activity of the one or more clients and the method further comprises dynamically adjusting an available pool of clients based on client responses.

13. The method as recited in claim 12, wherein dynamically adjusting includes removing clients that do not respond in accordance with a synchronization schedule and adding these clients back when these clients tender a response.

14. The method as recited in claim 9, wherein the master controller and the client controller are arranged for communication such that the clients communicate only with the master controller.

15. The method as recited in claim 9, wherein partitioning includes disjunctive partitioning wherein independent sub-problems are created deterministically by clients and solving includes statically solving an exclusive subset of sub-problems by clients.

16. The method as recited in claim 9, further comprising assigning a sub-problem by notifying a client of a partition depth and a corresponding BMC depth.

17. A system for bounded model checking of computer programs, comprising:

a master controller configured to control communication with one or more client controllers; and

a tunneling and slicing-based (TSR) BMC reduction method configured to decompose a computer program into sub-problems, the computer program having at least one reachable property node for bounded model checking (BMC);

the one or more client controllers configured to partition the sub-problems of the TSR method and solve the sub-problems independently of other clients to reduce communication overhead and provide scalability.

18. The system as recited in claim 17, wherein the master controller controls activity of the client controllers by dynamically adjusting an available pool of clients based on client responses, removing clients that do not respond in accordance with a synchronization schedule and adding these clients back when these clients tender a response.

19. The system as recited in claim 17, wherein the master controller and the client controllers are arranged in a star topology such that the client controllers communicate only with the master controller.

20. The system as recited in claim 17, wherein the one or more client controllers disjunctively partition independent sub-problems deterministically and solve an exclusive subset of the sub-problems statically.