Verifying compliance for business process logs with a hybrid logic model checker

Abstract

Given that organizations rely on the support of information systems in automating their business processes, the auditing of these processes is a complex task because it needs to consider both the business process model and the relevant data logs. For the compliance checking of such business situations, we present an extended version of a Hybrid Logics model checking tool, with temporal operators. The support for temporal operators allows for tracing the event logs and the verification of properties, within an abstract representation model corresponding to the intended concern of auditing.