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

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.

Having thus described the invention, what is claimed is:  
     
         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.