Analytical Software Design System

• US 20080263506A1
• Filed: 05/05/2005
• Published: 10/23/2008
• Est. Priority Date: 05/05/2004
• Status: Active Grant

• Current Assignee: Cocotec Limited
• Original Assignee: Silverdata Limited
• Inventors: Broadfoot, Guy Hampson, Hopcroft, Philippa Jane
• Granted Patent: US 8,370,798 B2
• Time in Patent Office: Days
• US Class Current: 717/104
• CPC Class Codes: G06F 8/10 Requirements analysis; Specification techniques
• CPC Class Codes: G06F 8/20 Software design
• CPC Class Codes: G06F 8/24 Object-oriented

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 behaviour; to analyse the mathematical models to determine if they have the required behaviour; to adjust the formal specifications until the required behaviour is achieved; and to derive the required verified design specifications from the mathematical models.

Claims

1-36. -36. (canceled)

37. 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, the system comprising:

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 behaviour;

to analyse the mathematical models to determine if they have the required behaviour;

to adjust the formal specifications until the required behaviour is achieved; and

to derive the required verified design specifications from the mathematical models.

38. A system according to claim 37, wherein the system is arranged to handle informal system design specifications comprising informal requirement specifications, informal architecture specifications and informal component and specification designs.

39. A system according to claim 38, wherein the black box specification generator is arranged to create formal interface specifications of the required functional behaviour of each component that is visible by its interfaces.

40. A system according to claim 39, wherein the black box specification generator is arranged to create the formal interface specifications as under-specified black-box specifications of the required functional behaviour.

41. A system according to claim 37, wherein the black box specification generator is arranged to create formal component design specifications of the required functional behaviour of each component.

42. A system according to claim 41, wherein the black box specification generator is arranged to create the formal component design specifications as fully specified black-box specifications of the required functional behaviour.

43. A system according to claim 41, wherein the black box specification generator is arranged to ensure that formal component design specifications are created to be compatible with the required interface behaviour.

44. A system according to claim 37, wherein the black box specification generator is arranged to generate a verified requirements specification, a verified architecture specification, a verified component design specification and a verified component interface specification.

45. A system according to claim 37, wherein the black box specification generator comprises a model generator for generating mathematical models representing the system behaviour.

46. A system according to claim 45, wherein the model generator is arranged to generate mathematical models in CSP notation.

47. A system according to claim 37, wherein the black box specification generator comprises a sequenced-based specification generator for processing the received informal system design specifications to create the formal specifications.

48. A system according to claim 47, wherein the sequenced-based specification generator is arranged to output analysis data for user consideration of the design specifications.

49. A system according to claim 37, wherein the black box specification generator comprises a model verifier for analysing the mathematical models to determine if they have the required behaviour.

50. A system according to claim 45, wherein

i) the model generator is arranged to generate mathematical models in CSP notation,

ii) the black box specification generator includes:

a sequenced-based specification generator for processing the received informal system design specifications to create the formal specifications; and

a model verifier for analysing the mathematical models to determine if they have the required behaviour, the model verifier including an FDR model checker for checking mathematical models described in CSP notation.

51. A system according to claim 45, wherein

i) the model generator is arranged to generate mathematical models in CSP notation,

ii) the black box specification generator includes:

a sequenced-based specification generator for processing the received informal system design specifications to create the formal specifications; and

a model verifier for analysing the mathematical models to determine if they have the required behaviour, the model verifier being arranged to feedback specification and design defects to the sequenced-based specification generator such that corrected formal specifications can be created to compensate for the defects, thereby enabling the model generator to create corrected mathematical models.

52. A system according to claim 50, wherein model verifier is arranged to feedback specification and design defects to the sequenced-based specification generator such that corrected formal specifications can be created to compensate for the defects, thereby enabling the model generator to create corrected mathematical models.

53. A system according to claim 37, further comprising an editor module arranged to enable user editing of the formal and informal specifications.

54. A system according to claim 53, wherein the editor module is arranged to store data as data files.

55. A system according to claim 37, further comprising an automated code generator for creating machine generated program source code from the verified specifications.

56. A system according to claim 37, further comprising an automated component test case generator for creating machine generated component test cases from the verified specifications.

57. A system according to claim 37, further comprising a verified implementation specification generator for creating verified implementation specifications from the verified specifications.

58. A system according to claim 57, wherein the verified implementation specification generator is arranged to process the received verified specifications to create formal implementation specifications;

to generate from the formal implementation specifications mathematical models representing the system implementation behaviour;

to analyse the mathematical models to determine if they have the required behaviour;

to adjust the formal implementation specifications until the required behaviour is achieved; and

to derive the required verified component implementation specifications from the mathematical models.

59. A system according to claim 58, wherein the system is arranged to process verified requirement specifications, verified architecture specifications and verified component design specifications.

60. A system according to claim 59, wherein the verified implementation specification generator is arranged to create formal implementation specifications meeting the verified requirement specifications.

61. A system according to claim 60, wherein the verified implementation specification generator is arranged to create the formal interface specifications as fully-specified black-box specifications of the required functional behaviour.

62. A system according to claim 58, wherein the verified implementation specification generator is arranged compare the verified component implementation specifications against the verified component design specifications and to detect and remove any errors found.

63. A system according to claim 58, wherein the verified implementation specification generator is arranged to carry out a box structure development method for creating formal implementation specifications.

64. A system according to claim 63, wherein the verified implementation specification generator comprises a model generator for generating mathematical models representing the system behaviour from the formal implementation specifications.

65. A system according to claim 64, wherein the model generator is arranged to generate mathematical models in CSP notation.

66. A system according to claim 58, wherein the implementation specification generator comprises a model verifier for analysing the mathematical models to determine if they have the required behaviour.

67. A system according to claim 63, wherein the implementation specification generator comprises a model verifier for analysing the mathematical models to determine if they have the required behaviour and the model verifier comprises an FDR model checker for checking mathematical models described in CSP notation.

68. A system according to claim 63, wherein the implementation specification generator comprises a model verifier for analysing the mathematical models to determine if they have the required behaviour and the model verifier is arranged to feedback specification and design defects to the verified implementation specification generator implementing the box-structured development method, such that corrected formal specifications can be created to compensate for the defects, thereby enabling the model generator to create corrected mathematical models.

69. A system according to claim 58, further comprising an editor module arranged to enable user editing of the formal implementation specifications.

70. A system according to claim 69, wherein the editor module is arranged to store data as data files.

71. A system according to claim 37 further comprising an interface protocol verifier generator for creating machine generated interface protocol verifiers from the verified specifications.

72. 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, the system being arranged to handle informal system design specifications comprising informal requirement specifications, informal architecture specifications and informal component and specification designs, the system comprising:

a verified black box specification generator arranged to;

process the received informal system design specifications to create formal specifications;

create formal interface specifications of a required functional behaviour of each component that is visible by its interfaces, the formal interface specifications being created as under-specified black-box specifications of the required functional behaviour;

generate from the formal specifications mathematical models representing the system behaviour;

analyse the mathematical models to determine if they have a required behaviour;

adjust the formal specifications until the required behaviour is achieved; and

derive the required verified design specifications from the mathematical models.

73. A system according to claim 72, wherein the black box specification generator is arranged to create formal component design specifications of the required functional behaviour of each component.

74. A system according to claim 72, wherein the black box specification generator comprises a sequenced-based specification generator for processing the received informal system design specifications to create the formal specifications.

75. A system according to claim 74, wherein the sequenced-based specification generator is arranged to output analysis data for user consideration of the design specifications.

76. A system according to claim 72, wherein the black box specification generator comprises a model verifier for analysing the mathematical models to determine if they have the required behaviour.

77. 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, the system comprising:

a verified black box specification generator arranged to;

process the received informal system design specifications to create formal specifications;

generate from the formal specifications mathematical models representing the system behaviour;

analyse the mathematical models to determine if they have the required behaviour;

adjust the formal specifications until the required behaviour is achieved; and

derive the required 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 mathematical models representing the system implementation behaviour;

analyse the mathematical models to determine if they have the required behaviour;

adjust the formal implementation specifications until the required behaviour is achieved; and

derive the required verified component implementation specifications from the mathematical models.

78. A method of carrying out analytical software design by receiving informal system design specifications and converting them 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 to create formal specifications;

generating from the formal specifications mathematical models representing the system behaviour;

analysing the mathematical models to determine if they have the required behaviour;

adjusting the formal specifications until the required behaviour is achieved; and

deriving the required verified design specifications from the mathematical models.

79. A data carrier having stored upon it a program for a computer for configuring the computer to implement the method as recited in claim 78.