Pattern Directed Auditing of Business Procedures: A Logic Programming, Model Checking Approach

Due to the stimulus from SOX as well as increasing use of computer-mediated workflows, automated methods for auditing internal control procedures are in increasing demand. Here we present a model checking technique for exhaustively analyzing internal control procedures to detect control weaknesses based on a specified set of control principles. We presume the control procedure to be represented in a computational format. Indeed, a computational version of the procedure currently in operation in the company may be directly accessible from the organization’s ERP and/or workflow system. By using logic-programming based pattern matching combined with model checking techniques we are able to identify sequences of actions in the procedure where the specified control principles are violated. Sample executions from our prototype system are included to demonstrate computational feasibility.