Method for automated error detection and verification of software

A computer program product, comprising:

• a computer readable medium having instructions stored thereon executable by a processor to perform a method for automated error detection and verification of software, the method comprising:
• providing a model of the software, the model comprising one or more model inputs and one or more model outputs, and a plurality of blocks embedded within the model each with an associated block type, the block types each having a plurality of associated block-level requirements;
• topologically propagating from the model inputs, a range of signal values or variable values, and error bounds, across computational semantics of all the blocks to the model outputs;
• identifying and examining each behavior pivot value for a given block to determine if modifying or extending the propagated range by the error bound will or may cause a signal value to fall on either side of the behavioral pivot value;
• and
• reporting all occurrences of the signal value that will or may fall on either side of the behavioral pivot value.

A system for automated error detection and verification of software, the system comprising:

• at least one processor;
• and
• at least one computer readable medium operatively coupled to the processor, the computer readable medium having instructions stored thereon executable by the processor to:
• provide a design model of the software, the design model comprising one or more model inputs and one or more model outputs, and a plurality of blocks embedded within the model each with an associated block type, the block types each having a plurality of associated block-level requirements;
• topologically propagate from the model inputs, a range of signal values or variable values, and error bounds, across computational semantics of all the blocks to the model outputs;
• identify and examine each behavior pivot value for a given block to determine if modifying or extending the propagated range by the error bound will or may cause the signal value to fall on either side of the behavioral pivot value;
• and
• report all occurrences of a signal value that will or may fall on either side of the behavioral pivot value.