Test postcondition items for automated analysis and test generation
AssigneeThe MathWorks, Inc.
InventorWilliam J. Aldrich
Life of this patent
Estimating the term…
Abstract
In one embodiment, a design is verified by creating a graphical model with a graphical modeling tool executing on a computing device. The graphical model may include a plurality of model elements. A postcondition element is coupled to a selected model element of the plurality of model elements. The postcondition element is associated with a desired result. The graphical model is employed to generate an executable form of the design. The executable form of the design and an indication of the desired result are provided to a verification tool, to instruct the verification tool to implement one or more verification scenarios.
Claims16
A method for verifying a design, performed by a computing device, the method comprising:
- creating, using a processor associated with the computing device, a graphical model of the design with a graphical modeling tool, where the graphical model includes a block diagram model that includes a plurality of model elements, where the plurality of model elements includes blocks interconnected by lines that represent signals;
- coupling, using the processor, a graphical postcondition element to a selected model element of the plurality of model elements, the graphical postcondition element including an indication of a desired result associated with the selected model element, where the graphical postcondition element corresponds to a block of the block diagram model;
- generating, using the processor, an executable form of the design from the graphical model;
- generating, using the processor, a postcondition specification based on the indication, where the postcondition specification is in a form usable by a verification tool;
- and
- providing, using the processor, the executable form of the design and the postcondition specification to the verification tool, to instruct the verification tool to implement one or more verification scenarios in which the selected model element produces the desired result.
A storage device comprising instructions executable by a computing device, the storage device comprising:
- one or more instructions to maintain a graphical model of a design, where the graphical model includes a block diagram model that includes a plurality of model elements, where the plurality of model elements includes blocks interconnected by lines that represent signals;
- one or more instructions to associate a graphical postcondition element with a selected model element of the plurality of model elements, the graphical postcondition element indicating one or more desired outputs associated with the selected model element where the graphical postcondition element corresponds to a block of the block diagram model;
- one or more instructions to generate an executable form of the design from the graphical model;
- one or more instructions to convert the graphical postcondition element into a form usable with the executable form of the design;
- and
- one or more instructions to provide the executable form of the design and the converted graphical postcondition element to a verification tool, to instruct the verification tool to implement one or more verification scenarios in which the selected model element produces the one or more desired outputs.
An apparatus comprising:
- means for creating a graphical model of a design, where the graphical model includes a block diagram model that includes a plurality of model elements, where the plurality of model elements includes blocks interconnected by lines that represent signals;
- means for associating a selected model element of the plurality of model elements with a graphical postcondition element indicating one or more desired outputs associated with the selected model element, where the graphical postcondition element corresponds to a block of the block diagram model;
- means for generating code from the graphical model, the code executable on a target device to implement functionality of the graphical model, where the means for generating code is to ignore the one or more desired outputs indicated by the graphical postcondition element when generating the code;
- and
- means for providing the generated code from the graphical model and an indication of the one or more desired outputs to a verification tool, to instruct the verification tool to implement one or more verification scenarios in which the selected model element produces the one or more desired outputs.
An apparatus comprising:
- a processor executing a graphical modeling tool, where the graphical modeling tool is to maintain a graphical model of a design, and where the graphical model includes a block diagram model that includes a plurality of model elements, where the plurality of model elements includes blocks interconnected by lines that represent signals;
- a display device that displays the graphical model to a user;
- an I/O device that permits a user to manipulate the graphical model to include a graphical postcondition element in the graphical model, where the I/O device further permits a user to set a desired result associated with the graphical postcondition element, and where the graphical postcondition element corresponds to a block of the block diagram model;
- and
- where the processor further executes a verification tool, where the verification tool receives an indication of the desired result from the graphical modeling tool and, in response thereto, directs verification of the graphical model to scenarios that produce the desired result.
Dependencies are inferred from the claim text.