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

• US 20030167182A1
• Filed: 07/22/2002
• Published: 09/04/2003
• Est. Priority Date: 07/23/2001
• Status: Abandoned Application

• Current Assignee: International Business Machines Corporation
• Original Assignee: International Business Machines Corporation
• Inventors: Wegman, Mark N., Bloom, Bard, Keyser, Paul T., Simmonds, Ian D.
• Application Number:
  US10/201,114
• Publication Number:
  US 20030167182A1
• Time in Patent Office: Days
• US Class Current: 705/1
• CPC Class Codes: G06F 8/10 Requirements analysis; Specification techniques
• CPC Class Codes: 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
• CPC Class Codes: G06Q 10/06375 Prediction of business process outcome or impact based on a proposed change
• CPC Class Codes: G06Q 10/067 Enterprise or organisation modelling
• CPC Class Codes: 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

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 application, 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

1. A method for determining if a business process satisfies certain properties, said method comprising the steps of:

building a model for the business process, the model comprising a plurality of actions each having at least one of a precondition and a postcondition;

constructing specifications for the properties, said specifications indicating both the states of the system and the order in which they may occur; and

determining if the model satisfies the specifications.

2. The method of claim 1 wherein said constructing specifications comprises consructing specifications in temporal logic for said model.

3. The method of claim 1 wherein failure to satisfy the specifications properties indicates a problem and wherein said method further comprising modifying at least one of said model, said business process, and said specifications to eliminate said problem.

4. The method of claim 1 wherein said determining if the model satisfies the specifications comprises the steps of:

comparing the outcomes of each of said plurality of actions to said specifications; and

verifying that said outcomes do not violate said states and said order.

5. 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.

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

7. The method of claim 1 wherein said determining if said model satisfies said specifications comprises running said specifications through an SMV model checking.

8. The method of claim 7 further comprising converting said specifications to SMV language prior to said running.

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

10. A method of specifying a business process comprising the steps of:

describing a multiple, dynamic classification scheme for objects; and

describing actions of the business process, each action having preconditions on the classifications of objects involved in the action, and specifying how objects'"'"' classifications change with performance of the action.

11. The method of claim 10 further comprising the step of generating an application that ensures that actions take place when valid.

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

13. A method for checking a business process for operating on a plurality of objects, said process being capable of attaining a plurality of states, comprising the steps of:

describing objects of said process using a dynamic multi-classification model;

describing actions that can take place in said process in terms of the classifications of the objects used in said actions;

describing how the classification of objects changes during actions; and

determining whether selected states of the business process are reachable based on said actions.

14. 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, the model comprising a plurality of actions each having at least one of a precondition and a postcondition;

constructing specifications in temporal logic for said model; and

determining if the model satisfies the specifications.

15. A program storage device readable by machine tangibly embodying a program of instructions executable by said machine for performing a method for specifying a business process, said method comprising the steps of:

describing a multiple, dynamic classification scheme for objects; and

describing actions of the business process, each action having preconditions on the classifications of objects involved in the action, and specifying how objects'"'"' classifications change with performance of the action.

16. The program storage device of claim 15 wherein said method further comprises the step of generating an application that ensures that actions take place when valid.

17. The program storage device of claim 15 wherein said method further comprises building an execution engine for said business process.

18. A program storage device readable by machine tangibly embodying a program of instructions executable by said machine for performing a method for checking a business process for operating on a plurality of objects, said process being capable of attaining a plurality of states, said method comprising the steps of:

describing objects of said process using a dynamic multi-classification model;

describing actions that can take place in said process in terms of the classifications of the objects used in said actions;

describing how the classification of objects changes during actions; and

determining whether selected states of the business process are reachable based on said actions.

19. A system 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 plurality of actions each having at least one of a precondition and a postcondition;

at least one specificatin component for constructing specifications for the properties, said specifications indicating both the states of the system and the order in which they may occur; and

at least one processing component for determining if the model satisfies the specifications.

20. A system for specifying a business process comprising the steps of:

at least one component for describing a multiple, dynamic classification scheme for objects; and

at least one component for describing actions of the business process, each action having preconditions on the classifications of objects involved in the action and for specifying how objects'"'"' classifications change with performance of the action.