The patent badge is an abbreviated version of the USPTO patent document. The patent badge does contain a link to the full patent document.
The patent badge is an abbreviated version of the USPTO patent document. The patent badge covers the following: Patent number, Date patent was issued, Date patent was filed, Title of the patent, Applicant, Inventor, Assignee, Attorney firm, Primary examiner, Assistant examiner, CPCs, and Abstract. The patent badge does contain a link to the full patent document (in Adobe Acrobat format, aka pdf). To download or print any patent click here.
Patent No.:
Date of Patent:
Jan. 01, 2019
Filed:
Apr. 06, 2016
General Electric Company, Schenectady, NY (US);
Han Yu, Clifton Park, NY (US);
Michael Richard Durling, Gansevoort, NY (US);
Kit Yan Siu, Saratoga Spring, NY (US);
Meng Li, Schenectady, NY (US);
Baoluo Meng, Iowa City, IA (US);
Scott Alan Stacey, Dayton, OH (US);
Daniel Edward Russell, Walker, MI (US);
Gregory Reed Sykes, Caledonia, MI (US);
GENERAL ELECTRIC COMPANY, Schenectady, NY (US);
Abstract
A computer-implemented system for generating test cases and/or test procedures to verify software having a nonlinear arithmetic constraint over a Real number range. The system includes a translator that receives, as input, software specification models for the software to be verified. The translator is configured to generate, as output, a plurality of SMT formulas that are semantically equivalent to the software specification models. The system includes an analytical engine pool that receives, as input, the plurality of SMT formulas from the translator and analyzes the plurality of SMT formulas, and generates, as output, test case data for each of the plurality of SMT formulas determined to be satisfiable. The system includes a post-processor that receives, as input, the test case data from the analytical engine pool and generates, as output, the test cases and/or test procedures for the software to be verified based on the test case data.