Microsoft Technology Licensing, LLC

Wolfgang Grieskamp

Wolfram Schulte

Nikolai Tillmann

Margus Veanes

Lev Borisovich Nachmanson

Colin L Campbell

Yuri Gurevich

Michael Barnett

Henricus Johannes Maria Meijer

Galen Clyde Hunt

James R Larus

Steven P Levi

John D DeTreville

Benjamin Zorn

Manuel Alfred Fahndrich

Thomas Michael Roeder

Nicolas Kicillof

Feng Chen

Andreas Blass

Nikolai Tillman

A finite domain approximation for symbolic terms of a symbolic state is derived, given some finite domains for basic terms of the symbolic state. A method is executed recursively for symbolic sub-terms of a symbolic term, providing a domain over-approximation that can then be provided to a solver for determining a more accurate domain. The method can be applied to a wide array of system terms, including, for example, object states, arrays, and runtime types.

Approximating finite domains in symbolic state exploration

A state component saves a present state of a program or model. This state component can be invoked by the program or model itself, thereby making state a first-class citizen. As the state of the program evolves from the saved state, the saved state remains for reflection and recall, for example, for testing, verification, transaction processing, etc. Using a state reference token, the saved state of the program or model can be accessed by the program or model. For example, the program or model by utilizing a state component, can return itself to the saved state. After returning to the saved state, a second execution path can be introduced without requiring re-execution of the actions leading to the saved state. In another example, the state space of an executing model is saved in order to generate inputs required to exercise a program or model.

State as a first-class citizen of an imperative language

Symbolic execution identifies possible execution paths of a computer program or method, each having certain constraints over the input values. The symbolic execution also records updates of memory locations, e.g. updates of the fields of symbolic objects in the heap of an object oriented program, involving a description of the previous heap, the updated symbolic object, a field identification, and a newly assigned symbolic value. The symbolic execution can also record calls to summarized methods, involving a description of previous calls, an identification of the summarized methods, and its symbolic arguments. The behavior of summarized methods can be expressed by axioms. Axioms describe the relationship between summarized methods under certain conditions. Axioms can be generated from parameterized unit tests. A parameterized unit test is a method with parameters which executes a sequence of calls to methods of an implementation under test; it asserts constraints over the inputs and outputs of the calls. A software testing program receives a parameterized unit test of an implementation under test, and symbolically executes the parameterized unit test. It can re-use axioms generated from other parameterized unit tests, and use them to emulate summarized methods.

Symbolic execution of object oriented programs with axiomatic summaries

A model composition environment can allow for description of fill or partial symbolic system behavior, as well as the combination of models of specific features into compound models. Compositional operators can include intersection, concatenation, substitution, alternating refinement, as well as a set of regular expression-like operators. Models called 'action machines' can represent object-oriented, reactive programs, and an action machine may be composed with another action machine using a compositional operator. This can allow for testing of particular scenarios or behaviors.

Symbolic program model compositions

A computerized method receives an implementation comprising a modifier method and an observer method of a class implementing an abstract data type. The method symbolically executes the modifier method to obtain constrained states, and applies the observer method in constrained states to obtain specialized axioms. The method then creates a specification from the obtained specialized axioms based on generalizing, merging and simplifying the specialized axioms.

Specification generation from implementations

Separation of parameterized unit tests (PUTs) from specific test cases supports many benefits including automated test case generation. Symbolic execution assigns symbolic input variables to parameters of a parameterized unit test. Path constraints of an implementation under test (IUT) are identified during symbolic execution. A constraint solver automatically generates test cases by determining the test inputs that satisfy one of more paths, each described by constraints, through the IUT. PUTs are used to populate behavioral summaries. Behavioral summaries are used later in future symbolic executions to emulate summarized methods. Behavioral summaries comprise behavioral purity axioms. Behavioral purity axioms require that an intensional heap before execution of a PUT be equal to the intensional heap after execution. An intensional heap is provided to represent state changes performed by summarized methods. The extensional heap is used to explicitly update memory locations, e.g. object fields or array elements.

Parameterized unit tests with behavioral purity axioms

Techniques and tools for testing multi-threaded or distributed software systems are described. For example, a multi-threaded system is instrumented and executed to produce logs of events that are performed by each of its agents. The agent logs contain a totally ordered series of events per agent, as well as information about accesses to resources shared between the agents. With this information, a partial ordering of the events performed by all the agents is described for the execution. The agent logs are then multiplexed into one or more serialized event orderings, which can then be compared to a specification of the system in a conformance testing engine.

Conformance testing of multi-threaded and distributed software systems

The present invention relates to a system and methodology to enable programming of generalized comprehensions in an imperative language environment. In one aspect, a system is provided to facilitate employment of user-definable and generalized comprehensions in accordance with imperative languages. The system includes a language component to enable programming of comprehension notations in an imperative language and an interface component to describe a meaning of the comprehension notations. A translation component facilitates execution of the comprehension notations in accordance with the imperative language.

Generalized comprehension in imperative languages

Described herein are methods and systems for interactively configuring and producing a data domain for various data structure elements of a computer program. A domain configuration manager is described which interactively receives domain configuration information corresponding to a data structure element, reads a reflection of the program and produces a data domain according to domain configuration information. The domain configuration manager is capable of producing a data domain for a data structure element according to such domain configuration information such as an explicit expression, inheritance or domain generation technique. The reflection of the computer program exposes the methods and functions of the program to be used in the explicit expression regardless of the visibility rules. Also, predicates and conditions can be used with domain generation techniques to further narrowly configure the data domains.

Interactive domain configuration

Techniques and tools for generating test cases for methods or programs with input preconditions are described. For example, after finding feasible control flow paths for a tested method along with each path's associated input conditions, a new program is created which tests these conditions along with the precondition. By analyzing this new program's control flow graph, a class of test cases is found while avoiding inefficiencies created by doing complete searches of paths through the combined control flow graph of the precondition and the method. Additional efficiencies are introduced by partitioning a control flow graph for the precondition into branched and straight sections.

Generating test cases for software with complex preconditions

A computerized method creates test coverage for non-deterministic programs. The method receives a graph of edges and states representing a program under test, and creates a continuous cycle of edges that reaches each edge in the graph at least once. In one example, the method splits the continuous cycle into discrete sequences that end at edges reaching non-deterministic nodes in the graph, and verifies that the executing program conforms to the behavior represented by the discrete sequences. In another example, a method creates probabilistic strategies for reaching one or more vertices in a non-deterministic graph. The strategies provide a graph path with a high probability of reaching a desired vertex.

Non-deterministic testing

A computer system provides a test program and one or more unit tests, such as a traditional unit test and or a parameterized unit test. The system also includes a constraint solver, a theorem prover, an implementation under test, a symbolic executor, a generalizor, and generated test cases. The generalizor receives a traditional unit tests as input, and modifies the traditional unit test into a parameterized unit test. The modification includes replacing plural concrete values in the traditional unit test with symbols, and exporting the symbols into a signature of the parameterized unit test. A symbolic executor identifies constraints while symbolically executing the created parameterized unit test of the implementation under test. A constraint solver and or theorem prover generates a set of test cases by solving for values that satisfy the series of constraints. The test program executes the automatically generated test cases.

Unit test generalization

Constraints are defined in view of a program implementation. Constraints check program state or variables to maintain data consistency. A constraint component determines a constraint's scope and variables upon which a constraint depends. Program flow is altered so constraints are checked whenever a variable upon which a constraint depends is updated. Optionally, program flow is altered dynamically to re-establish constraints whenever a variable upon which a constraint depends is updated. Re-establishing constraints provides efficiency, since a program flow is altered for a minimum cost based on a present evolving minimum set of active constraint-variable relationships.

Efficient checking of state-dependent constraints

Techniques and tools for generating finite state machines ('FSMs') for a software system with asynchronous callbacks are described. For example, method invocations in a model of the software system are partitioned into observable and controlled method invocations. The controlled method invocations are those which can be run from a test harness while the observed method invocations are those which are observed asynchronously as they are invoked in the system. An FSM is created with observation and control nodes such that observable transitions are found from observation nodes and controlled transitions are found from control nodes. If a state of the model contains both controlled and observable invocations, a timeout transition is added to the FSM to give an implementation time to come up with an observed method invocation before continuing to controlled invocations.

Growing community of inventors

Redmond, WA, United States of America

Wolfgang Grieskamp