Symbolic program model compositions
AssigneeMicrosoft Corporation
InventorsColin L. Campbell, Margus Veanes, Nicolas Kicillof, Nikolai Tillmann, Wolfgang Grieskamp, Wolfram Schulte
Life of this patent
Estimating the term…
Abstract
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.
Claims14
A computer-implemented method of creating a software program model, the method comprising:
- defining a first symbolic program model;
- defining a second symbolic program model;
- defining a symbolic model operator;
- combining the first symbolic program model with the second symbolic program model according to a set of rules of the symbolic model operator and properties of the second symbolic program model to produce the software program model comprising one or more states;
- and
- observing properties of the software program model using a test program and a symbolic explorer that prunes exploration of the software program model based on state subsumption.
A computer-readable medium containing instructions which can cause a computer to perform a method, the method comprising:
- defining a symbolic program model;
- defining a symbolic scenario model;
- defining a symbolic model operator;
- and
- modifying the symbolic program model according to properties of the symbolic model operator and according to properties of the symbolic scenario model producing a software program model comprising one or more states;
- wherein the one or more states of the software program model are examined using a test program in conjunction with a symbolic explorer that prunes a search of the software program model based on state subsumption.
A system for testing programs comprising:
- a digital processor;
- and
- a digital memory, the memory comprising:
- a symbolic program model;
- a symbolic scenario model;
- a symbolic model operator, wherein the processor is configured to modify the symbolic program model according to one or more properties of the symbolic model operator and according to one or more properties of the symbolic scenario model to produce a software program model with one or more states;
- a test program;
- an explorer that prunes a search of the software program model based on state subsumption, wherein the test program is configured to examine the one or more states of the software program model in conjunction with the explorer;
- and
- a program model source, wherein the symbolic program model is derived from the program model source.
Dependencies are inferred from the claim text.