Automated method for building and maintaining software including methods for verifying that systems are internally consistent and correct relative to their specifications

• US 6,275,976 B1
• Filed: 02/25/1997
• Issued: 08/14/2001
• Est. Priority Date: 03/15/1996
• Status: Expired due to Term

• Current Assignee: Joseph M. Scandura
• Original Assignee: Joseph M. Scandura
• Inventors: Scandura, Joseph M.
• Primary Examiner(s): Chaki, Kakali
• Application Number:
  US08/805,694
• Time in Patent Office: 1,631 Days
• Field of Search: 395/701-704, 395/500.43, 714/36, 714/38, 706/25-30, 706/919-923, 703/22
• US Class Current: 717/120
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013
• CPC Class Codes: G06F 11/3696 Methods or tools to render software testable

Abstract

Software development and maintenance involves assembling components, sometimes with explicit support during the design process but more frequently not. In neither case has it been possible to ensure internal consistency and correctness in a manner that scales well to large as well as small system.

The invention disclosed herein is an intuitive, repeatable, formally verifiable and automated method for developing and maintaining software systems that is practical and easy to use. Specifically, this method provides human designers with automated support for specifying, designing, implementing and maintaining arbitrarily large, complex software systems that are both internally consistent and logically correct (i.e., consistent with external specifications). This method avoids the “combinatorial explosion” problem and minimizes the need for human input, respectively, by constructing specifications and solution designs via successive levels of refinement and by categorizing input and output values into equivalence classes.

Claims

1. A computer implemented method for specifying, designing, testing, implementing and maintaining at least one of a plurality of systems that can be guaranteed to be internally consistent and abstractly correct with respect to their specifications via successive refinement, said method comprising the steps of:

a) building and maintaining a specification hierarchy representing a behavioral system in which input and output variables have been hierarchically structured so that abstract behavior of said behavioral system at successive levels of refinement in said specification hierarchy is equivalent in response to a request to specify the behavior of said system;

b) in response to a request building and maintaining a design hierarchy corresponding to the behavioral system in which each refinement in said design hierarchy conforms to consistency constraints, which guarantee that the children in each said refinement produce behavior that is abstractly equivalent to that of the parent, wherein each design in said design hierarchy produces abstract behavior equivalent to a corresponding specification hierarchy hierarchy when said specification hierachy of step a) exists;

c) analyzing at least one of said specification hierarchy and said design hierarchy in response to a request to extract information inherent in at least one of said specification hierarchy and said design hierarchy;

d) modifying said specification hierarchy in response to a request to modify the abstract behavior of said specification hierarchy;

e) modifying said design hierarchy in response to a request to modify the abstract behavior of said design hierarchy;

f) testing at least one design in response to a request subsequent to at least one of the steps of dynamically modeling the behavior of said design and creating test cases for said design and proving conclusively that a component in at least one said design executes according to its specification;

g) in response to a request implementing at least one component by converting said components in said design into executables; and

h) in response to a request performing at least one of the steps of executing said design, calling said design from an existing application and executing a component or a design corresponding to at least one component in said design.

2. A method in accordance with claim 1, further comprises the steps of:

a1) specifying at least one output variable, and for each said output variable in said specification hierarchy, specifying zero or one input variable and at least one input variable to said specification hierarchy which maps into said output variable;

b1) partitioning the values of each said input and output variable of said specification hierarchy into equivalence classes, said partition consisting of a finite number of abstract values, one abstract value being the default number;

c1) specifying a mapping of said abstract input values of step b1, into said abstract output values;

d1) given one of an input variable and an output variable in said specification hierarchy, refining said variable into one of no child variables, said variable then being terminal in said specification hierarchy, and one of component child variables and category child variables and relationships between child variables and operations, specifying mappings between input and output child variables, said components, categories, relationships and operations more fully characterizing said input and output variables;

e1) specifying a mapping between the abstract values of each said parent variable of step d1) and the abstract values of said children variables of said parent variable;

f1) for each said child output variable of step d1), specifying a mapping from said abstract values of said input children variables of step d1 ) into said abstract values of each said child output variable; and

g1) ensuring that said input and output mappings of step c1) are consistent with said child mappings of step a1), in which case the mapping of step e1) followed by the mapping of step c1) generates the same abstract values for each said output variable of step c1) as does the mapping of step f1) followed by the mapping of step e1).

3. A method in accordance with claim 2, wherein said step d1) of refining each said input and output variable into child variables further comprises:

a2) when said refinement is a component refinement, distinguishing between prototype component refinements in which one child component represents a finite set of child components, each of which has exactly the same structure and the same abstract values, and those said component refinements which are not said prototype refinements; and

b2) when said refinement is a category refinement, distinguishing between category refinements in which all child variables are atomic, without any internal component structure, and those said category refinements In which at least one said child variable has component variables.

4. A method in accordance with claim 2 for constructing a higher order specification hierarchy when the values of at least one said variable of claim 2 are specifications.

5. A method in accordance with claim 2 for constructing specifications for real time systems wherein the values of at least one variable of said specification are themselves one of time and timed events.

6. A method in accordance with claim 1 wherein said step b) of building a design hierarchy by successive refinement of design components in which each refinement in said hierarchy conforms to consistency constraints, which guarantee that the children In each refinement produce behavior that is abstractly equivalent to that of the parent, wherein each design component in said hierarchy produces abstract behavior equivalent to said specification when said specification hierarchy of step a) of claim 1 exists, further comprises the steps of:

a1) constructing and choosing a name for a top-level design component in said design hierarchy, in which the parameters of said top-level design component include all of the input and output variables at the top-level of said specification hierarchy of claim 1, and when said specification hierarchy of claim 1 hierarchy exists, said design component also including as parameters one of no external events and input events and their abstract values from outside said design hierarchy;

b1) refining each design component of said design hierarchy into one of a sequence, parallel, selection, iteration, affiliate, relation and operation refinement in accordance with specified consistency constraints, wherein said consistency constraints ensure that the abstract behavior of each said design component is equivalent to the abstract behavior of the child design components in said refinement;

c1) for each parameter of each said child design component of step b) which is not identical to a variable in said specification hierarchy of claim 1 or a parameter of the parent design component of said refinement of step b), partitioning the values of said parameter into abstract values, one said abstract value being the default, and specifying the abstract input-output behavior for each said design component in said each refinement, the full set of input and output parameters of each child design component in said each refinement comprising the specifications for said child design component;

d1) verifying that the abstract behavior specified by each parent design component in each said refinement is consistent with the abstract behavior specified by the children design components in each said refinement; and

e1) when said specification hierarchy of step a) of claim 1 exists, repeating steps b1) through d1) until all variables in said specification hierarchy of step a) of claim 1 have been referenced in said design hierarchy.

7. A method in accordance with claim 6 wherein said step b1) of refining said design component into one of a sequence, parallel, selection, iteration, affiliates, relation and operation, in accordance with specified constraints on design refinements, wherein said specified constraints on design refinements ensure consistency of said refinement, further comprises the steps of,

a1) when at least one parameter of said design component corresponds to a variable in said specification hierarchy of claim 6, herein called a specification parameter

(I) selecting one said specification parameter of said design component,

(ii) determining the specification refinement type of said specification parameter, and

(iii) suggesting the type of refinement of said design component as follows;

when the type of said specification parameter is a component refinement, then suggesting a parallel refinement for said design component,

when the type of said specification parameter is a prototype refinement representing a variable number of components, then suggesting a loop refinement for said design component,

when the type of said specification parameter is a prototype refinement representing a fixed number of components, then suggesting a navigation sequence refinement for said design component,

when the type of said specification parameter is a terminal refinement with at least two abstract values, then suggesting a case refinement for said design component, otherwise make no said suggestion,

when the type of said specification parameter is a category refinement with atomic sub-categories, then suggesting one of a selection and case refinement for said design component,

when the type of said specification parameter is a category refinement with non-atomic sub-categories, otherwise known as a class inheritance hierarchy, then suggesting an affiliate refinement for said design component

when the type of said specification parameter is an relational refinement, otherwise known as a extraction refinement, then suggesting a sequence refinement for said design component,

when the type of said specification parameter is a dynamic refinement, then suggesting an interactional refinement for said design component;

(iv) choosing a refinement type for said design component,

(v) verifying that said refinement type is consistent with said specification hierarchy, wherein said consistency means;

when the refinement type of said design component is a parallel refinement, then at least one of said specification parameter of said design component must be one of a terminal refinement and a component refinement,

when the refinement type of said design component is a loop refinement, then at least one specification parameter of said design component must be one of a terminal refinement and a prototype refinement representing a variable number of components,

when the refinement type of said design component is a navigation sequence refinement, then at least one specification parameter of said design component must be one of a terminal refinement and a prototype refinement representing a fixed number of components,

when the refinement type of said design component is one of a case refinement and a selection refinement, then at least one specification parameter of said design component must be one of a terminal refinement and a category refinement with atomic sub-categories,

when the refinement type of said design component is a case refinement, then at least one specification parameter of said design component must be one of a terminal refinement and an atomic category refinement,

when the refinement type of said design component is an affiliate refinement, in which at least one parameter of said design component is an object, wherein said design component is an abstract design component, then at least one specification parameter of said design component must be one of a terminal refinement and a non-atomic category refinement,

when the refinement type of said design component is a sequence refinement, then at least one specification parameter of said design component must be one of a terminal refinement and a relational refinement,

when the refinement type of said design component is an interactional refinement, then at least one specification parameter of said design component must be one of a terminal refinement and a dynamic refinement, and

b2) for said refinement of step a2), checking to ensure that consistency constraints for the refinement type of said refinement are satisfied, and ensuring that the abstract behavior of said design component is equivalent to the abstract behavior of the child design components in said refinement.

8. A method in accordance with claim 6 for constructing a higher order design hierarchy when the values of at least one parameter of said design component of claim 6 are design components.

9. A method in accordance with claim 6 for constructing designs for real time system wherein the values of at least one variable of a design are themselves one of time and timed events.

10. A method in accordance with claim 1 wherein said step of maintaining said specification hierarchy of step a) of claim 1 in which input and output variables have been hierarchically structured so that abstract behavior at successive levels of refinement is equivalent, further comprises the steps of,

a1) modifying the abstract input-output behavior of at least one variable in said specification hierarchy;

b1) updating the abstract input-output behavior of the parent and the children of said variable of step a) to maintain abstract consistency;

c1) updating refinements in which said parent is a child and in which those said children which are changed are parents; and

d1) repeating step c1) until there are no more parent variables and no more children which are changed.

11. A method in accordance with claim 1 wherein said step of modifying a design hierarchy in which the behavior of the parent and children In each said refinement is equivalent, further comprises the steps of:

a1) modifying the abstract behavior of a design component in said design hierarchy;

b1) updating the parent of said design component in accordance with the consistency constraints of the refinement containing said parent and ensuring that the abstract behavior of the parent and children in said refinement is equivalent and updating the children of said design component in accordance with the consistency constraints of the refinement containing said design component and ensuring that the abstract behavior of said design component and its children is equivalent;

c1) updating the parent in those refinements in which said parent is a child when said parent has been changed;

d1) updating the children in those refinements in which said child is a parent when said child has been changed; and

e1) repeating step c1) and d1) until there are no more parent and child design components.

12. A method in accordance with claim 11 wherein said step c1) of updating the parent of said design component in said design hierarchy further comprises the steps of:

a2) identifying the parent of said design component in said design hierarchy,

b2) identifying the type of refinement associated with said parent; and

c2) constructing a parent design component for said refinement of step b2) from the children of said refinement using consistency constraints specified for said type of refinement of step b2).

13. A method in accordance with claim 12 wherein the step of constructing a parent design component from children design components further comprises:

a) for each sequence refinement In said program, using consistency constraints for sequences to construct the patent design component in said sequence refinement;

b2) for each selection refinement in said program, using consistency constraints for selections to construct the parent design component in said selection refinement;

c3) for each loop refinement in said program, using consistency constraints for loops to construct the parent design component in said loop refinement; and

d3) when said refinement is a loop refinement, said loop refinement contains one of an unelaborated loop body and a condition and an advance operation, an action operation and a condition.

14. A method in accordance with claim 13 wherein said step of constructing a parent design component from said children design components in said sequence refinement further comprises:

a4) identifying those subsequences of said refinement that are navigation sequences and those subsequences of said sequence refinement that are parallel refinements;

b4) inserting into Said design hierarchy of claim 13 a parent for each said subsequence, said subsequence parent replacing its children in said sequence and updating the contents of each said subsequence parent; and

c4)c) updating said sequence refinement.

15. A method in accordance with claim 14 wherein said step of identifying those subsequences of said sequence that are navigation sequences and those subsequences of said sequence that are parallel refinements further comprises:

a5) one of not partitioning the design components in said sequence refinement and partitioning Said sequence into navigation sub-sequences which introduce alias variables and non-navigation sequences, which do not introduce said aliases, and using consistency constraints to convert navigation sub-sequences into navigation sequence refinements;

b5) for each non-navigation sequence and each navigation sequence refinement in said program, one of not partitioning said sequences and partitioning said sequences into sub-sequences of steps which must be carried out sequentially and those sub-sequences which may be carried out in parallel, and

c5) when a said subsequence may be carried out in parallel, using consistency constraints to construct a parent design component for said parallel refinement, wherein new higher level parameters, composed of component variables in child design components, may be introduced in said parent design component.

16. A method in accordance with the method of claim 11, which creates an internally consistent design hierarchy from a design that has been constructed using traditional methods of assembling design components, wherein said design is constructed from design components in a canonical form, including refinement types and wherein goto'"'"'s have been eliminated, wherein said design defines an implicit design hierarchy whose higher level elements include the successively embedded refinement types in said design and wherein higher level design components in said implicit design hierarchy are constructed from said design, said method comprising the steps of,

a2) embedding said design in an implicit design hierarchy;

and

b2) applying the method claim 11 to each refinement in said implicit design hierarchy, wherein each child of each said refinement is a design component in one of said design and said implicit design hierarchy, to construct a parent design component in said refinement.

17. A method for converting the steps in a plurality of programs into components represented in said canonical form of claim 16, wherein said programs are written in a structured programming language in which goto'"'"'s have been eliminated, wherein said programs may be one of program, subroutine, function, affiliate operation or method associated with an object, callback and remote procedure call, and wherein said canonical form means that each design component is an operation or function, whose input and output parameters are typeless and which does not reference any global variables, said method comprising the steps of;

a) receiving said program;

be) converting global variables used in said program to parameters and insuring that said program consists entirely of modules;

c3) converting each statement in each module in said program into a design component represented in said canonical form wherein the type of each parameter of each said canonical design component is represented as a data structure of typeless data elements and the input, output and Input-output role of each said parameter is represented in said canonical form, and

d3) reverse engineering, said program to extract the implicit design hierarchy of refinement types defined by said program.

18. A method in accordance with claim 1 wherein the step of testing at least one design by one of dynamically modeling the behavior of said design, creating test cases for said design and proving that a design component executes correctly, wherein said design may be at any level of abstraction in said design hierarchy, wherein parameters of said design components may have multiple data types in which case said design components are called abstract design components, further comprises:

a1) selecting a design

b1) the dynamically modeling the behavior of said design comprising,

(I) when said design element is an abstract design component, then determining which affiliates to invoke at run-time based on the structure of the parameters and replacing said design component with a sequence whose elements are affiliate design components,

(ii) when said design component is not executable, then presenting an external agent with the input values of the parameters of said design component, and obtaining the corresponding output values and data structures of said parameters from said external agent,

(iii) when said design component is executable, then executing said design component,

(iv) repeating steps (i) through (iii) until there are no more design components to interpret;

c1) in response to a request to create test cases for said design wherein said test cases can be used to ensure that said design produces behavior consistent with said specification of claim 1,

(i) selecting at least one set of actual values for each combination of abstract values of input variables in said specification of claim 1 associated with said selected design, wherein each said set contains one actual value for each said abstract value of input variables;

(ii) for each combination of said abstract values of input variables of said step (i), determining the corresponding set of abstract output values of output variables in said specification of claim 1, each said combination of actual input values of step (i) and said corresponding abstract output values constituting a test case; and

(iii) applying said test cases of step c1 (ii) to said design of step a1) and determining whether each actual output value belongs to said corresponding abstract value of output variables of step c1) (ii) for said corresponding test case; and

d1) in response to a request to prove conclusively that a given design component executes according to its specification,

(i) selecting a verification method including at least one of formal proofs, automated theorem proving techniques and other verification methods;

(ii) when at least one of formal proofs and automated theorem proving techniques is selected in said step d1) (i) and the specification of said design component is not sufficiently precise to allow use of at least one of said formal proofs and automated theorem proving techniques, then

identifying variables in said specification of said design component whose abstract values are too abstract to allow proof and

introducing a relational refinement, also called an extract refinement, wherein the specification of the children in said relational refinement is represented as a relationship between two or more variables, wherein said relationship is sufficiently precise, wherein said relationship is expressed in some suitable logic, for use in at least one of said formal proofs and automated theorem proving techniques.

19. A method in accordance with claim 1, wherein step g) of implementing at least one component in a design in a manner which guarantees abstract correctness, said method comprising the steps of:

a) in response to a request, one of receiving and identifying and constructing a finite set of design components sufficient for implementing all contemplated design components in a given set of designs;

b) in response to a request, receiving an unimplemented design component and converting said design component into a problem whose input consists of the specification for said design component and whose goal is satisfied by designs consistent with asid specification;

c) in response to a request, deriving a design component from said finite set of components consistent with said specification of said design component of step b); and

d) in response to a request, when absolute correctness must be guaranteed, verifying that said derived design component executes correctly; and

e) in response to a request, repeating steps b) through d) until all design components in said design of step b) have been implemented.

20. Given a design in a design hierarchy Implemented in accordance with the method of claim 19, a method for implementing an equivalent design in said design hierarchy, in which said equivalent design is at least one of faster in execution and more compact in size;

said method compricing the steps of;

a2) when the designer seeks to speed execution,

(I) identifying a portion of said design, commonly known as a section of code, which Is operating slower than desired,

(ii) identifying that design component, which is at a higher level of abstraction In said design hierarchy and which is the parent of a sub-hierarchy in said design hierarchy which includes said identified section of code,

(iii) implementing said higher level design component in a lower level language and

(iv) when the designer seeks to eliminate redundancy, at least one of deleting unused local variables in said design and replacing a local variable used in one subtree of said design hierarchy with a reusable local variable used in a preceding subtree of said design hierarchy;

b2) when the designer seeks to make said design more general,

(I) identifying a component in said design, wherein at least one original parameter of said given component may be replaced by another parameter, said another parameter having the same commonly understood “

real world”

meaning and representing a set of data structures, which includes the data structure of said original parameter,

(ii) replacing said original parameter with said another parameter and converting said design component into an abstract design component and constructing a class hierarchy, including affiliates that support all data structures associated with said another parameter.

21. A method in accordance with claim 19, wherein said step of constructing a finite set of design components sufficient for implementing all contemplated designs, wherein said finite set of design components consists of lower and higher order design components, and wherein said lower and higher design components collectively provide a sufficient basis for constructing designs that satisfy an arbitrarily diverse set of specifications in some implicitly, but ill-defined domain of problems, further comprises

a2) constructing a finite sample of specifications in said ill-defined domain;

b2) constructing a design component for each specification in said finite sample of step a);

c2) for each said design component, one of converting and not converting said design into a higher order specification;

d2) constructing a higher order design component for each said higher order specification;

e2) one of repeating steps c) and d) and not repeating said steps.

22. A method in accordance with claim 21, wherein said step c) of converting said design into a higher order specification further comprises:

a) for each said design of step b) of claim 21, identifying corresponding Input designs from which said design can be constructed;

be) for each said design of step a), constructing a pair consisting of the specification for said design and the set of input designs of step a) that map into said design;

c3) partitioning said pairs of step b) into equivalence classes using at least one of artificial intelligence, another automated technique and designer judgment; and

d3) converting each said equivalence class of step c) into a higher order specification, wherein the inputs and output in said higher order specification are at least one of an abstraction and a generalization of a corresponding pair.

23. Given a problem, wherein the input to said problem is the specification for a to-be-implemented design component, together with a finite set of available components, and the goal in said problem Is a design that satisfies said specification, a method in accordance with claim 19 wherein the step of deriving said design from said finite set of available components further comprises the steps of:

a2) finding a component in said finite set of available components, which matches said problem, wherein the output of said component contains the specification of said problem at a specified level of outputs in said specification said initial level being one;

b2) when said component is found, then applying said component to said Input to said problem and said set of available components and adding the design generated by said component to the set of available components and decrementing the level of outputs in said specification which said finding of step a) searches;

c2) when said component of step a) is not found, then incrementing the level of outputs at which said finding searches; and

d2)repeating said steps a2)a) through c2) until one of said component of Step a) is found and said level of outputs reaches some prescribed number.

24. A method in accordance with claim 23, wherein said problem may be any of a plurality of problems, wherein the input to said problem may be any given, the set of available components may be any set of problems, the goal in said problem may be any goal and a solution to said problem is a design that operates on said given and generates an output that satisfies said goal of said problem.

25. A method in accordance with claims 23, wherein said step of finding a component whose specification matches said solution, further comprises:

a) a) when a component has the desired behavior but the interface is not in a prescribed canonical form, then semantically wrapping said component to conform to said canonical form.

26. A method in accordance with claim 1, wherein a specification hierarchy is constructed from a design hierarchy constructed in accordance with step b), wherein each kind of design refinement corresponds one-to-one with a unique specification refinement, said method comprising the steps of:

a1) when said design hierarchy has no explicit specification, select the top level input and output variables in said design hierarchy as said specification;

b1) for each refinement in said design hierarchy of each said variable, identifying the refinement type, the children variables of said refinement, and the abstract values of said children variables in said design refinement;

c1) converting the type of said design refinement into the corresponding specification refinement type and adding said converted refinement type, including its children variables and abstract values, to said specification hierarchy; and

d1) repeating steps b1) and c1) until one of all said children variables have been identified and converted and said specification has otherwise been deemed by some human or intelligent agent to be sufficiently detailed.

27. A method by which designs constructed in accordance with step h) of claim 25, wherein said design can be utilized within or in conjunction with one of a plurality of existing designs, components, applications and operating systems, said method comprising at least one of the steps of:

a) executing said design;

b) when one of said application and said operating system calls a component corresponding to said design, then converting calls from one of said application and said operating system into calls on said design; and

c) when said design calls a design component, which can be implemented using at least one of the steps of calling an existing design, calling an executable component, calling an application and calling an operating system, then replacing said design component in said design with one of said existing design, component, application and operating system.