Analytical software design system
First Claim
1. 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.
5 Assignments
0 Petitions
Accused Products
Abstract
An analytical software design system arranged to receive informal system design specifications and to convert them into verified design specifications for use in creating source code and carrying out implementation testing of the source code is described. The system comprises a verified black box specification generator arranged to process the received informal system design specifications to create formal specifications; to generate from the formal specifications mathematical models representing the system behavior; to analyze the mathematical models to determine if they have the required behavior; to adjust the formal specifications until the required behavior is achieved; and to derive the required verified design specifications from the mathematical models.
32 Citations
45 Claims
-
1. 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. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33)
-
-
34. An analytical software design system arranged to receive informal system design specifications of a software system and to convert them into verified design specifications for use in creating source code and carrying out implementation testing of the source code, the software design system being arranged to handle informal system design specifications comprising informal requirement specifications, informal architecture specifications and informal component and specification designs, the software design system comprising:
-
a verified black box specification generator including a processor to; process the received informal system design specifications; for each component of the software system, create a formal design specification representative of a fully-specified black box function; create formal interface specifications of required run-time interface behavior of each of the components that is visible by its interfaces, the formal interface specifications being created as under-specified black-box specifications of the required run-time interface behavior which captures non-deterministic behavior present at the respective interfaces of the each component with all other components with which the component interacts; generate from the formal design specifications and the formal interface specifications, for each of the components, a mathematical model representing run-time system behavior for the component with all other components with which the component interacts; analyse the mathematical models to determine if the mathematical models have required run-time system behavior; adjust at least one of the formal design specifications or the formal interface specifications until the required run-time system behavior is achieved; and derive the verified design specifications from the mathematical models. - View Dependent Claims (35, 36, 37, 38)
-
-
39. An analytical software design system arranged to receive informal system design specifications of a software system and to convert the informal system design specifications into verified design specifications for use in creating source code and carrying out implementation testing of the source code, the software design system comprising:
-
a verified black box specification generator arranged to; process the received informal system design specifications and for each component of the software system to create formal specifications representative of a fully-specified black box function; generate from the formal specifications mathematical models representing run-time system behavior of the software system; analyse the mathematical models to determine if the mathematical models have required run-time system behavior; adjust the formal specifications until the required run-time system behavior is achieved; and derive verified design specifications from the mathematical models; and a verified implementation specification generator for creating verified implementation specifications from the verified specifications, the verified implementation specification generator being arranged to; process the received verified specifications to create formal implementation specifications; generate from the formal implementation specifications, for each of the components, a mathematical model representing run-time implementation behavior for the component with all other components with which the component interacts; analyse the mathematical models representing the run-time implementation behavior to determine if the mathematical models representing the run-time implementation behavior have required run-time implementation behavior; adjust the formal implementation specifications until the required run-time implementation behavior is achieved; and derive the verified implementation specifications from the mathematical models representing the run-time implementation behavior, wherein at least one of the verified black box specification generator and the verified implementation specification generator includes a processor. - View Dependent Claims (40, 41)
-
-
42. A method of carrying out analytical software design by receiving informal system design specifications of a software system and converting the informal system design specifications into verified design specifications for use in creating source code and carrying out implementation testing of the source code, the method comprising:
-
processing the received informal system design specifications and for each component of the software system creating formal design specifications representative of a fully-specified black box function; creating formal interface specifications of required run-time interface behavior of each of the components that is visible by its interfaces, the formal interface specifications being created as under-specified black-box specifications of the required run-time interface behavior which captures non-deterministic behavior present at the respective interfaces of the each component with all other components with which the component interacts; generating from the formal design specifications and the formal interface specifications, for each of the components, a mathematical model representing run-time system behavior for the component with all other components with which the component interacts; analysing the mathematical models to determine if the mathematical models have required run-time system behavior; adjusting at least one of the formal design specifications or the formal interface specifications until the required run-time system behavior is achieved; and deriving the verified design specifications from the mathematical models, wherein at least one of the processing, the creating, the generating, the analyzing, the adjusting and the deriving is by a processor. - View Dependent Claims (43)
-
-
44. A non-transitory data carrier having stored thereon a program for a computer for configuring the computer to implement a method of carrying out analytical software design by receiving informal system design specifications of a software system and converting the informal system design specifications into verified design specifications for use in creating source code and carrying out implementation testing of the source code, the method comprising:
-
processing the received informal system design specifications and for each component of the software system creating formal design specifications representative of a fully-specified black box function; creating formal interface specifications of required run-time interface behavior of each of the components that is visible by its interfaces, the formal interface specifications being created as under-specified black-box specifications of the required run-time interface behavior which captures non-deterministic behavior present at the respective interfaces of the each component with all other components with which the component interacts; generating, from the formal design specifications and the formal interface specifications, for each of the components, a mathematical model representing run-time system behavior for the component with all other components with which the component interacts; analysing the mathematical models to determine if the mathematical models have required run-time system behavior; adjusting at least one of the formal design specifications or the formal interface specifications until the required run-time system behavior is achieved; and deriving the verified design specifications from the mathematical models. - View Dependent Claims (45)
-
Specification