Patent 07979848 - Systems, methods and apparatus for pattern matching in procedure development and verification > Claims

1. A non-transitory computer-accessible medium having executable instructions to validate a system, the computer-accessible medium executable instructions capable of directing a processor to perform: receiving scenarios of the system;pattern-matching the scenarios of the system to at least one process-based specification segment; andanalyze the formal specification,wherein the computer executable instructions comprise pattern-matching the scenarios of the system to a formal specification, in reference to an inference engine, applying mathematical logic to the formal specification in order to identify a presence or absence of mathematical properties of the scenario, and correcting the absence of the mathematical properties if the mathematical properties are identified as absent in the scenario, andwherein the mathematical properties of the formal specification comprise whether the formal specification implies a system execution trace that includes a deadlock condition, whether the formal specification implies a system execution trace that includes a livelock condition, and whether the formal specification implies a system execution trace that exhibits or does not exhibit a plurality of other desirable or undesirable behaviors including, but not limited to safety properties, security properties, unreachable states, inconsistencies, naming conflicts, unused variables, unexecuted code.
- 2. The non-transitory computer-accessible medium of claim 1, wherein the formal specification further comprises a process algebra.
  - 3. The non-transitory computer-accessible medium of claim 2, wherein the process algebra comprises a language of Communicating Sequential Processes.
4. A non-transitory computer-accessible medium having executable instructions to generate a system from scenarios, the executable instructions capable of directing a processor to perform: pattern-matching a plurality of scenarios to a formal specification; and translating the formal specification to a process-based specification implementing the system,wherein the mathematical properties of the formal specification comprise whether the formal specification implies a system execution trace that includes a deadlock condition, whether the formal specification implies a system execution trace that includes a livelock condition, and whether the formal specification implies a system execution trace that exhibits or does not exhibit a plurality of other desirable or undesirable behaviors including, but not limited to safety properties, security properties, unreachable states, inconsistencies, naming conflicts, unused variables, unexecuted code.
- 5. The non-transitory computer-accessible medium of claim 4, wherein the executable instructions further comprise: verifying the syntax of the plurality of scenarios; andmapping the plurality of scenarios to a plurality of formal specification segments.
- 6. The non-transitory computer-accessible medium of claim 4, wherein the executable instructions further comprise: verifying consistency of the formal specification.
- 7. The non-transitory computer-accessible medium of claim 4, wherein the executable instructions further comprise: analyzing the formal specification.
- 8. The non-transitory computer-accessible medium of claim 4, wherein the executable instructions further comprise: determining mathematical and logical properties of the formal specification by an automated inference engine.
- 9. The non-transitory computer-accessible medium of claim 4, wherein the executable instructions further comprise: pattern-matching the plurality of scenarios to a separate formal specification without the use of an automated inference engine.
- 10. The non-transitory computer-accessible medium of claim 4, wherein the formal specification further comprises a process algebra.
  - 11. The non-transitory computer-accessible medium of claim 10, wherein the process algebra comprises a language of Communicating Sequential Processes.
12. A system to validate a software system, the system comprising: a processor;an inference engine;a pattern-matcher operable to receive a plurality of scenarios of the software system and to generate in reference to the inference engine a specification encoded in a formal specification language; andan analyzer, operable to perform model verification/checking and determine existence of omissions, deadlock, livelock, and race conditions or other problems and inconsistencies in the formal specification,wherein the mathematical properties of the formal specification comprise whether the formal specification implies a system execution trace that includes a deadlock condition, whether the formal specification implies a system execution trace that includes a livelock condition, and whether the formal specification implies a system execution trace that exhibits or does not exhibit a plurality of other desirable or undesirable behaviors including, but not limited to safety properties, security properties, unreachable states, inconsistencies, naming conflicts, unused variables, unexecuted code.
- 13. The system of claim 12, wherein the pattern-matching of the scenarios into a specification is carried out without human intervention.
14. A non-transitory computer-accessible medium having executable instructions to validate a system, the executable instructions capable of directing a processor to perform: receiving scenarios of the system; pattern-matching the scenarios of the system to a formal specification; andtranslating the formal specification to an implementation,wherein the executable instructions further comprise analyzing the formal specification and applying mathematical logic to the formal specification in order to identify a presence or absence of mathematical properties of the formal specification, andwherein the mathematical properties of the formal specification further comprise whether the formal specification implies a system execution trace that includes a deadlock condition, whether the formal specification implies a system execution trace that includes a livelock condition, and whether the formal specification implies a system execution trace that exhibits or does not exhibit a plurality of other desirable or undesirable behaviors including, but not limited to safety properties, security properties, unreachable states, inconsistencies, naming conflicts, unused variables, unexecuted code.
- 15. The non-transitory computer-accessible medium of claim 14, wherein the executable instructions further comprise: pattern-matching the scenarios of the system to the formal specification, without the use of an automated inference engine.
- 16. The non-transitory computer-accessible medium of claim 14, wherein the executable instructions further comprise: pattern-matching the scenarios of the system to the formal specification, in reference to an inference engine.
- 17. The non-transitory computer-accessible medium of claim 14, wherein the formal specification further comprises a process algebra.
  - 18. The non-transitory computer-accessible medium of claim 17, wherein the process algebra comprises a language of Communicating Sequential Processes.
- 19. The non-transitory computer-accessible medium of claim 14, wherein the executable instructions further comprise pattern-matching the scenario to a formal model; and translating the formal model to at least one scenario.
20. A non-transitory computer-accessible medium having executable instructions to validate a system, the executable instructions capable of directing a processor to perform: receiving a formal model of the system; andpattern-matching the formal model to a scenario,wherein the executable instructions further comprise analyzing the formal model and applying mathematical logic to the formal model in order to identify a presence or absence of mathematical properties of the formal model, andwherein the mathematical properties of the formal model comprise whether the formal model implies a system execution trace that includes a deadlock condition, whether the formal model implies a system execution trace that includes a livelock condition, and whether the formal model implies a system execution trace that exhibits or does not exhibit a plurality of other desirable or undesirable behaviors safety properties, security properties, unreachable states, inconsistencies, naming conflicts, unused variables, unexecuted code.
- 21. The non-transitory computer-accessible medium of claim 20, wherein the executable instructions further comprise translating the formal model to at least one scenario.
- 22. The non-transitory computer-accessible medium of claim 20, wherein the formal model further comprises a process algebra.
- 23. The non-transitory computer-accessible medium of claim 20, wherein the process algebra comprises a language of Communicating Sequential Processes.
24. A non-transitory computer-accessible medium having executable instructions to validate a system, the executable instructions capable of directing a processor to perform: receiving a scenario of the system; andpattern-matching the scenario to a formal model,wherein the executable instructions further comprise analyzing the formal model and applying mathematical logic to the formal model in order to identify a presence or absence of mathematical properties of the formal model, andwherein the mathematical properties of the formal model comprise whether the formal model implies a system execution trace that includes a deadlock condition, whether the formal model implies a system execution trace that includes a livelock condition, and whether the formal model implies a system execution trace that exhibits or does not exhibit a plurality of other desirable or undesirable behaviors including, but not limited to safety properties, security properties, unreachable states, inconsistencies, naming conflicts, unused variables, unexecuted code.
- 25. The non-transitory computer-accessible medium of claim 24, wherein the formal model further comprises a process algebra.
  - 26. The non-transitory computer-accessible medium of claim 25, wherein the process algebra comprises a language of Communicating Sequential Processes.
27. A non-transitory computer-accessible medium having executable instructions to validate a system, the executable instructions capable of directing a processor to perform: pattern-matching a plurality of scenarios to a plurality of formal models;combining the plurality of formal models to a singular formal model;analyzing the singular formal model;correcting the absence of mathematical properties in the singular formal model; andtranslating the formal model to an implementation,wherein the executable instructions further comprise applying mathematical logic to the singular formal model in order to identify a presence or absence of mathematical properties of the singular formal model, andwherein the mathematical properties of the singular formal model comprise whether the singular formal model implies a system execution trace that includes a deadlock condition, whether the singular formal model implies a system execution trace that includes a livelock condition, and whether the singular formal model implies a system execution trace that exhibits or does not exhibit a plurality of other desirable or undesirable behaviors including, but not limited to safety properties, security properties, unreachable states, inconsistencies, naming conflicts, unused variables, and unexecuted code.