FORMAL ANALYSIS DRIVEN BASED EVOLUTION OF REQUIREMENTS SPECIFICATIONS
A method for developing a specification includes receiving a plurality of requirements that define the functionality of the specification, wherein the plurality of requirements are expressed using a formal model. The method further includes analyzing the plurality of requirements using algorithms and determining if the plurality of requirements satisfies a predetermined set of criteria. The method further includes generating a summary of the formal analysis and refining the requirements by incorporating corrected analysis results.
1 . A method for developing a specification, the method comprising the steps of:
receiving a plurality of requirements that define the functionality of the specification, wherein the plurality of requirements are expressed using a formal model;
simulating the plurality of requirements using formal analysis;
determining if the plurality of requirements satisfies a predetermined set of criteria;
generating a summary of the formal analysis; and
modifying at least one of the plurality of requirements if at least one of the predetermined set of criteria is not satisfied.
2 . The method of claim 1 , further including modifying the generated summary and using this modified summary as a specification item, thereby refining the specification.
3 . The method of claim 2 , further including iteratively refining the specification using feedback provided by the formal analysis.
4 . The method of claim 3 , wherein the steps of simulating the plurality of requirements, determining if the requirements satisfy the set of criteria, and generating a summary are repeated using the modified summary.
5 . The method of claim 1 , wherein the summary of the formal analysis indicates if the plurality of requirements satisfies the predetermined set of criteria.
6 . The method of claim 1 , wherein simulating the plurality of requirements using formal analysis includes analyzing the requirements using at least one algorithm.
7 . The method of claim 1 , wherein determining if the plurality of requirements satisfies a predetermined set of criteria includes determining if the requirements are at least one of complete, correct, consistent and non-ambiguous.
8 . The method of claim 1 , further including amending the portion of the requirements that does not satisfy the predetermined set of criteria.
9 . The method of claim 8 , further including incorporating the amended portion of the requirements into the specification.
10 . The method of claim 1 , wherein the formal model is in the form of a state machine, a scenario or structured English.
11 . The method of claim 1 , wherein the modified summary is incorporated into the specification to refine the specification.
12 . A method, comprising the steps of:
receiving a plurality of requirements that define the functionality of a specification, wherein the plurality of requirements are expressed using a formal model;
testing the plurality of requirements for defects using formal analysis;
generating a summary that includes the results of the formal analysis; and
refining the plurality of requirements by incorporating the results of the formal analysis into the specification as specification items.
13 . The method of claim 12 , wherein testing the plurality of requirements for defects using formal analysis includes determining the behavior of the specification.
14 . The method of claim 13 , wherein refining the plurality of requirements based on the results of the formal analysis includes correcting defects by specifying an expected defect-free summary.
15 . The method of claim 14 , further including incorporating the expected defect-free summary into the specification.
16 . The method of claim 12 , wherein testing the plurality of requirements for defects using formal analysis includes analyzing the requirements using at least one algorithm.
17 . The method of claim 12 , wherein testing the plurality of requirements for defects includes determining if the plurality of requirements is one or more of incomplete, incorrect, inconsistent or ambiguous.
18 . A system for developing a specification, the system comprising:
a database configured to receive a plurality of requirements; and
an analysis engine configured to simulate the plurality of requirements using formal analysis, wherein the formal analysis identifies defects in the requirements;
wherein the requirements are refined to correct the defects and the refined requirements are incorporated into the specification.
19 . The system of claim 18 , wherein the analysis engine generates a summary of the formal analysis.
20 . The system of claim 18 , wherein the formal analysis applies a plurality of algorithms to the requirements to determine if the requirements are at least one of incomplete, incorrect, inconsistent or ambiguous.