# US 10,310,819 B2 · Method and apparatus for providing symbolic mode checking of business application requirements

> Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt

- Number: US 10,310,819 B2
- Document ID: US10310819B2
- Status: Granted
- Kind: B2
- Application number: 12/544,933
- Filed: 2009-08-20
- Published: 2009-12-17
- Granted: 2019-06-04
- Earliest claimed: 2001-07-23
- Assignees: International Business Machines Corporation
- Applicants: Bard Bloom; Ian D. Simmonds; Paul T. Keyser; Mark N. Wegman
- Inventors: Bard Bloom; Ian D. Simmonds; Paul T. Keyser; Mark N. Wegman
- Web page: https://patentgrep.com/patent/US10310819B2

## CPC

- G06F 8/10: Requirements analysis; Specification techniques
- G06Q 10/0637: Strategic management or analysis, e.g. setting a goal or target of an organisation; Planning actions based on goals; Analysis or evaluation of effectiveness of goals
- G06Q 10/06375: {Prediction of business process outcome or impact based on a proposed change}
- G06Q 10/067: Enterprise or organisation modelling
- Y04S 10/50: Systems or methods supporting the power network operation or management, involving a certain degree of interaction with the load-side end user applications
- G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N)
- G06Q: INFORMATION AND COMMUNICATION TECHNOLOGY [ICT] SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL OR SUPERVISORY PURPOSES; SYSTEMS OR METHODS SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL OR SUPERVISORY PURPOSES, NOT OTHERWISE PROVIDED FOR
- Y04S: SYSTEMS INTEGRATING TECHNOLOGIES RELATED TO POWER NETWORK OPERATION, COMMUNICATION OR INFORMATION TECHNOLOGIES FOR IMPROVING THE ELECTRICAL POWER GENERATION, TRANSMISSION, DISTRIBUTION, MANAGEMENT OR USAGE, i.e. SMART GRIDS

## Abstract

A system and method for providing symbolic mode checking of business application requirements. A language allows for building a model for the business process, the model comprising a plurality of actions, with each action having a precondition and a postcondition or outcome. Specifications are constructed for the properties of the business applications with the specifications describing both the states of the business process and the order in which they may occur. Finally, the model and the specifications are analyzed to determine if the model satisfies the specifications. If the model fails to satisfy the specifications, a problem may be indicated in the business application. The process can be automated to permit the system to make assumptions for conducting a thorough analysis of selected potential problem areas in the application.

## Claims

### Claim 1

A computer-implemented method for a processing system for determining if business process application software satisfies certain predetermined properties, said method comprising the steps of:
said processing system:
building a model for the business process application software, the model comprising:
a data model of objects in a multiple dynamic classification hierarchy wherein objects may have multiple classes, and
a control model comprising a plurality of actions on the objects each having a body of code and at least one of a pre-condition and a post-condition;
constructing specifications as finite state programs for predetermined properties, said specifications being statement in branching temporal logic and indicating both states of the business process with temporal connectives and an order in which the states may occur;
determining that the model satisfies the specifications for the predetermined properties, wherein the determination comprises:
parsing the specifications and converting the specifications to SMV (Symbolic Model Verifier) language;
running the specifications through an SMV model checking; and
comparing the outcomes of each of the plurality of actions to the specifications to determine whether the outcomes violate said states and said order;
modifying at least one of said model, the business process, and the specifications when the model fails to satisfy the specifications; and
iteratively repeating said determining that the model satisfies the specifications and said modifying until no outcomes violate said states and said order.

### Claim 2 (depends on 1)

The method of claim 1 wherein said constructing specifications for the properties comprises the steps of:
describing objects in multiple, dynamic classifications;
describing process actions in terms of the classifications of the objects used in the actions; and
describing how the classifications of objects change during actions.

### Claim 3 (depends on 2)

The method of claim 2 wherein said describing objects comprises expressing data about individual objects in classification and expressing data about several entities in terms of relationships and maps.

### Claim 4 (depends on 1)

The method of claim 1 further comprising building an execution engine for said business process.

### Claim 5 (depends on 1)

The method of claim 1 further comprising annotating actions and outcomes with costs and probabilities to facilitate said modifying.

### Claim 6 (depends on 1)

The method of claim 1 wherein constructing specifications comprises expressing conditions for actions as one of conjunction, disjunction, implication, equivalence, an n-ary operating for precisely one of, and an n-ary operation for at most one of.

### Claim 7

A program storage device readable by machine tangibly embodying a program of instructions executable by said machine for performing a method of determining if a business process satisfies certain properties, said method comprising the steps of:
building a model for the business process application software, the model comprising a data model of objects in a multiple dynamic classification hierarchy wherein objects may have multiple classes and a control model comprising a plurality of actions on the objects each having a body of code and at least one of a pre-condition and a post-condition;
constructing specifications as finite state programs for predetermined properties, said specifications being statement in branching temporal logic and indicating both states of the business process with temporal connectives and an order in which the states may occur;
determining that the model satisfies the specifications for the predetermined properties, wherein the determination comprises:
parsing the specifications and converting the specification to SMV (Symbolic Model Verifier) language;
running the specification through an SMV model checking; and
comparing the outcomes of each of the plurality of actions to the specifications to determine whether the outcomes violate said states and said order; and
modifying at least one of said model, the business process, and the specifications when the model fails to satisfy the specifications.

### Claim 8

A computer system having at least one processing device for determining if a business process satisfies certain properties, comprising:
at least one building component for building a model for the business process, the model comprising a data model of objects in a multiple dynamic classification hierarchy wherein objects may have multiple classes and a control model comprising a plurality of actions on the objects each having a body of code and at least one of a pre-condition and a post-condition;
at least one specification component for constructing specifications as finite state programs for predetermined properties, said specifications being statement in branching temporal logic and indicating both states of the business process with temporal connectives and an order in which the states may occur;
at least one processing component for determining that the model satisfies the specifications for the predetermined properties, wherein the determination comprises:
parsing the specifications and converting the specifications to SMV (Symbolic Model Verifier) language;
running the specifications through an SMV model checking; and
comparing the outcomes of each of the plurality of actions to the specifications to determine whether the outcomes violate said states and said order; and
wherein at least one of said model, said business process, and said specifications when the model fails to satisfy the specifications to eliminate said problem.