A model-checking approach to analysing organisational controls in a loan origination process