Patent ID: 8370798

Claim:
An analytical software design system comprising: a verified black box specification generator including a processor arranged to enable received informal design specifications of a software system to be developed for each component of the software system into: (i) formal design specifications representative of a fully-specified black box function; and (ii) formal interface specifications representative of an under-specified black box specification of required run-time interface behavior which captures non-deterministic behavior present at respective interfaces of the each component with all other components with which the component interacts, wherein the verified black box specification generator is arranged to test correctness of the formal design specifications and the formal interface specifications and to generate verified design specifications; the verified black box specification generator comprising: input screen units for capturing the formal specifications as sequenced-based specifications using input screens, in which input entries of the input screens each identify a stimulus, a response and an equivalence; a model generator arranged to generate automatically, for each of the components, a mathematical model of run-time system behavior for the component with all other components with which the component interacts from the formal design specifications and the formal interface specifications expressed in the input screens; and a model verifier arranged to analyze the mathematical models to determine if the mathematical models have required run-time system behavior for the corresponding components, to identify errors in the formal interface specifications and the formal design specifications, and to feedback the errors into at least one of the informal or formal design specifications; wherein the verified black box specification generator is arranged to enable user adjustment of the formal interface specifications and the formal design specifications via the input screens to generate corrected mathematical models respectively for the components, to analyze the corrected mathematical models, to identify errors, to feedback the errors until the required run-time system behavior for the corresponding component is achieved, and to derive the verified design specifications from error-free mathematical models.