Analytical software design system

An analytical software design system comprising:

• a verified 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;
• and
• (ii) formal interface specifications of required run-time interface behavior which capture run-time behavior present at respective interfaces of the each component with all other components with which the component interacts,
• the verified specification generator comprising:
• 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;
• 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 specification generator is arranged to enable user adjustment of the formal interface specifications and the formal design specifications 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.

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 specification generator including a processor to:
• process the received informal system design specifications;
• for each component of the software system, create formal design specifications;
• 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 specifications of the required run-time interface behavior which captures run-time 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.

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 specification generator arranged to:
• process the received informal system design specifications and for each component of the software system to create formal design specifications;
• generate from the formal design 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 design 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 specification generator and the verified implementation specification generator includes a processor.

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;
• 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 capturing run-time 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.

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;
• 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 specifications of the required run-time interface behavior which captures run-time 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.