Analysis and verification of distributed applications
First Claim
1. A computing system comprising at least one computing node and at least one data store in communication with the at least one computing node, the at least one data store having stored therein computer instructions that, upon execution by the at least one computing node, at least cause the system to:
- receive an application program operable to execute in a distributed computing environment;
parse the application program in accordance with one or more verification constraints and based on the parsing;
divide the application program into a plurality of independently executable components; and
determine an initial set of test inputs to the independently executable components;
instantiate a plurality of virtual machines and execute the independently executable components in respective ones of the virtual machines;
modify a non-deterministic event in order to effectuate a deterministic result in accordance with one or more determinism policies in response to a determination that the non-deterministic event has occurred between at least two of the virtual machines;
in response to a determination that application data is to be communicated between at least two of the virtual machines;
generate a data packet that encapsulates the application data along with associated condition variables and data path information;
send the data packet to a destination for the data packet; and
aggregate application data and combine respective condition variable and data path information;
verify one or more verification objectives by using the aggregated application data to represent code execution paths; and
iteratively generate new test inputs based on the verifying until the one or more verification objectives are validated.
1 Assignment
0 Petitions
Accused Products
Abstract
Systems and methods are described for analyzing and verifying distributed applications. In one embodiment, an application program is parsed and a set of inputs is determined. The application program is executed as one or more independently executable components. During execution, non-deterministic events are modified in order to effectuate a deterministic result. Redundant portions of the set of inputs are aggregated, and the set of inputs is iteratively updated.
43 Citations
22 Claims
-
1. A computing system comprising at least one computing node and at least one data store in communication with the at least one computing node, the at least one data store having stored therein computer instructions that, upon execution by the at least one computing node, at least cause the system to:
-
receive an application program operable to execute in a distributed computing environment; parse the application program in accordance with one or more verification constraints and based on the parsing; divide the application program into a plurality of independently executable components; and determine an initial set of test inputs to the independently executable components; instantiate a plurality of virtual machines and execute the independently executable components in respective ones of the virtual machines; modify a non-deterministic event in order to effectuate a deterministic result in accordance with one or more determinism policies in response to a determination that the non-deterministic event has occurred between at least two of the virtual machines; in response to a determination that application data is to be communicated between at least two of the virtual machines; generate a data packet that encapsulates the application data along with associated condition variables and data path information; send the data packet to a destination for the data packet; and aggregate application data and combine respective condition variable and data path information; verify one or more verification objectives by using the aggregated application data to represent code execution paths; and iteratively generate new test inputs based on the verifying until the one or more verification objectives are validated. - View Dependent Claims (2, 3, 4, 5)
-
-
6. A computer-implemented method for verifying a property of a distributed application program, comprising:
-
parsing an application program in accordance with one or more constraints for application program conditions; executing the application program as independently executable components resulting from division of the application program, wherein the independently executable components are executed using an initial set of inputs determined based on the parsing and symbolic evaluation of the independently executable components; during the executing, modifying a non-deterministic event occurring between at least two of the independently executable components in order to effectuate a deterministic result; and generating new inputs based on the executing. - View Dependent Claims (7, 8, 9, 10, 11, 12, 13, 14, 15, 16)
-
-
17. One or more non-transitory computer-readable storage media having collectively stored thereon executable instructions that, when executed by one or more processors of a computer system, cause the computer system to:
-
parse an application program in accordance with one or more constraints for application program conditions, wherein the application program is divided into independent components that can be executed as independent processes; execute the independent components in independent execution environments, wherein the independent components are executed using an initial set of inputs determined based on symbolic evaluation of the independent components; during execution, modify non-deterministic events in order to effectuate deterministic results; and identify unexecuted portions of the components and generate new inputs. - View Dependent Claims (18, 19, 20, 21)
-
-
22. A computing system comprising one or more computing nodes and one or more data stores in communication with the one or more computing nodes, the one or more data stores having stored thereon computer instructions that, upon execution by the one or more computing nodes, at least cause the computing system to:
-
parse an application program in accordance with one or more constraints for application program conditions; cause execution of the application program as independently executable components resulting from division of the application program, wherein the independently executable components are executed using an initial set of inputs determined based on the parsing and symbolic evaluation of the independently executable components; during the execution, modify a non-deterministic event occurring between at least two of the independently executable components in order to effectuate a deterministic result; and generate new inputs based on the execution.
-
Specification