Exploring the Alloy operational semantics for case management process modeling

Efficient case management in industry is hampered by attempts to deal with case management process the same way as with regular business process. Development of the specific approaches for case management process modeling and analysis is therefore an important endeavor that can improve the case management practice. In this work, we provide a mathematical model and a comprehensible formalism for reasoning about the meaning - the semantics - of case management process. We represent case management process as a finite state machine (FSM) and express its operational semantics in the Alloy specification language. The Alloy Analyzer tool allows us to define, simulate and validate a case management process model while efficiently managing its complexity. We illustrate our findings on the example of Mortgage Approval process.