Analysis and verification of distributed applications

摘要

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.

主权项

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; anddetermine 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; andaggregate 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.