GENERATING AND UTILIZING FINITE INPUT OUTPUT MODELS, COMPARISON OF SEMANTIC MODELS AND SOFTWARE QUALITY ASSURANCE

• US 20070266366A1
• Filed: 03/29/2007
• Published: 11/15/2007
• Est. Priority Date: 05/12/2006
• Status: Abandoned Application

• Current Assignee: Phase Change Software LLC
• Original Assignee: Iosemantics, LLC
• Inventors: Bucuvalas, Steven
• Application Number:
  US11/693,491
• Publication Number:
  US 20070266366A1
• Time in Patent Office: Days
• US Class Current: 717/104
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013
• CPC Class Codes: G06F 11/3612 by runtime analysis performance monitoring G06F11/3466
• CPC Class Codes: G06F 8/427 Parsing
• CPC Class Codes: G06F 8/433 Dependency analysis; Data or control flow analysis

Abstract

Aspects of the invention relate generally to software, and more specifically to one or more specifically to software development, FIOSM creation, comparison and subsumption in a software environment and software quality assurance. An exemplary embodiment includes the processes of: (i) designing and verifying that a computer language can completely and correctly generate a Finite Input-Output Semantic Model (FIOSM); and (ii) generating, typically using automation, a FIOSM for a program or system of several programs written in a FIOSM-compatible language.

Claims

1. A method for generating a finite input/output semantic model comprising:

receiving a source program;

parsing the source program into an abstract data structure;

generating a set of code paths based on the abstract data structure;

converting the set of code paths into a set of logically consistent data element models;

utilizing the set of logically consistent data element models to format the finite input/output semantic model including;

identifying a set of input data elements in the source program,

identifying a set of output data elements in the source program, and

for each set of data elements, creating an input-output pattern expression;

producing a valid data expression for each set of input data elements; and

producing a valid data expression for each set of output data elements.

2. The method of claim 1, wherein the source program is written in programming language having unambiguous semantics and decidable and complete data flow.

3. The method of claim 1, wherein the source program is written in programming language wherein each operator of a set consisting of all operators in the language has unambiguous semantics and is incapable of an invoking infinite code path.

4. The method of claim 1, wherein the source program is written in programming language wherein each operator of a set consisting of all operators in the language is incapable of an invoking infinite code path.

5. The method of claim 1, wherein the abstract data structure comprises a parse tree.

6. The method of claim 1, wherein the abstract data structure comprises a tree model.

7. The method of claim 1, wherein the abstract data structure comprises a directed acyclic graph structure.

8. The method of claim 7, wherein said generating a set of code paths based on the abstract data structure comprises walking the parse tree.

9. The method of claim 7, wherein said generating a set of code paths based on the abstract data structure comprises using a suitable algorithm to walk the parse tree.

10. A method of creating a computer language wherein a set of all programs created in the language have a decidable and complete data flow comprising:

designing the language including defining operators and defining data types; and

verifying the decidable and complete data flow.

11. The method of claim 10, wherein defining operators includes only specifying operators whose semantics are not ambiguous or cannot invoke infinite code paths.

12. The method of claim 10, wherein the data types comprise enumerable and non-enumerable data types.

13. The method of claim 12, wherein all data elements of the non-enumerated data types are represented as sets.

14. The method of claim 13, wherein all data elements consisting of infinite sets are expressed with a finite lexical notation.

15. The method of claim 14, wherein numeric data types are non-enumerated data types and numeric data elements of the numeric data types are expressed using equalities and/or inequalities.

16. The method of claim 10, wherein verifying decidable and complete data flow comprises verifying both a code path quality and a data flow quality of the language.

17. The method of claim 16, wherein said verifying a code path quality comprises demonstrating all possible code paths within the language can be expressed in a finite tree model.

18. The method of claim 17, wherein the tree model comprises a directed acyclic graph.

19. The method of claim 17 wherein said demonstrating all possible code paths within the language comprises generating a tree model using a tableau algorithm.

20. The method of claim 16, wherein verifying the data flow quality further comprises identifying a set of one or more complete and correct algorithms that can determine the value of any data element in the set of all programs written in the language.

21. The method of claim 20, wherein said identifying a set of one or more complete and correct algorithms comprises demonstrating a valid algorithm for each data type associated with the language.

22. The method of claim 21, wherein said demonstrating a valid algorithm for each data type comprises utilizing automated algebraic analysis.

23. The method of claim 21, wherein said demonstrating a valid algorithm for each data type comprises utilizing approximation.

24. The method of claim 10, further comprising repeating said designing the language after said verifying the decidable and complete data flow if decidable and complete data flow is unverifiable.

25. The method of claim 24, wherein the operations of designing and verifying are repeated iteratively until decidable and complete data flow is verified.

26. The method of claim 10, wherein defining control flow operators includes only specifying control flow operators whose semantics are not ambiguous or result in infinite code paths.

27. A method for quality control of software comprising:

generating a parse tree;

generating a code path set based on the parse tree;

generating a path data model set using the code path set; and

generating a finite input/output semantic model (FIOSM) from the path data model set.

28. The method of claim 27, wherein the generation of a finite input/output semantic model dictates that the software has a completely decidable data flow.

29. The method of claim 27, wherein said generating a parse tree comprises parsing the source code of a software procedure.

30. The method of claim 27, wherein said generating a parse tree comprises parsing the source code of a software program.

31. One or more of a program, routine, language, sub-routine, procedure, software enterprise system, module and portion of code having a completely decidable data flow.

32. A method of software quality assurance comprising analyzing one or more finite input output semantic models of computer code.

33. The method of claim 32, wherein the analyzing comprises a regression process.

34. The method of claim 32, wherein the analyzing comprises determining policy compliance.

35. The method of claim 33, wherein the regression process comprises:

determining a finite input output semantic model for a first portion of computer code;

determining a subset of the finite input output semantic model, wherein the subset is one or more input/output pattern definitions; and

determining a finite input output semantic model for the one or more input/output pattern definitions.

36. The method of claim 34, wherein a policy provides a constraint on input/output behavior of the computer code.

37. The method of claim 36, wherein the policy has an input/output signature corresponding to the computer code it references.

38. The method of claim 34, wherein policy creation comprises:

determining a policy to represent at least one user-defined policy, wherein the policy is a finite input output semantic model; and

storing the policy.

39. The method of claim 33, further comprising testing the regression process including:

obtaining the finite input output semantic model for the computer code;

loading a regression set;

comparing the finite input output semantic model for the computer code and the regression set; and

determining whether the regression set is a subset of the finite input output semantic model for the computer code.

40. The method of claim 34, wherein testing of policy compliance comprises:

obtaining the finite input output semantic model for the computer code;

loading a policy;

performing a comparison process to determine which input/output pattern definitions in the finite input output semantic model have input patterns which subsume an input pattern of a policy finite input output semantic model; and

performing a comparison process to determine which input/output patterns from the above comparison process are subsumed by an output pattern of the finite input output semantic model for the policy.

41. A method of software quality assurance comprising analyzing one or more finite input output semantic models of a program in cooperation with a policy validation user interface.

42. A software development tool comprising:

a semantic model generator;

a model comparator; and

a quality assurance monitor,

wherein the semantic model generator determines if a program has a completely decidable data flow.

43. A software development tool comprising:

a semantic model generator, the semantic model generator verifying a complete a decidable data flow in a program.

44. The tool of claim 43, further comprising a model comparator.

45. The tool of claim 43, further comprising a quality assurance monitor.

46. A method for generating a finite input/output semantic model comprising:

receiving a set of source code, the set of source code comprising at least one of a program, a procedure, a routine, a module, and a software enterprise system;

parsing the source code into an abstract data structure;

generating a set of code paths based on the abstract data structure;

converting the set of code paths into a set of logically consistent data element models;

utilizing the set of logically consistent data element models to format the finite input/output semantic model including;

identifying a set of input data elements in the source code,

identifying a set of output data elements in the source code, and

for each set of data elements, creating an input-output pattern expression;

producing a valid data expression for each set of input data elements; and

producing a valid data expression for each set of output data elements.