Method and apparatus for providing symbolic mode checking of business application requirements

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.

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.