TY - GEN
T1 - On-the-fly auditing of business processes
AU - Van Hee, Kees
AU - Hidders, Jan
AU - Houben, Geert J.
AU - Paredaens, Jan
AU - Thiran, Philippe
PY - 2010
Y1 - 2010
N2 - Information systems supporting business processes are usually very complex. If we have to ensure that certain business rules are enforced in a business process, it is often easier to design a separate system, called a monitor, that collects the events of the business processes and verifies whether the rules are satisfied or not. This requires a business rule language (BRL) that allows to verify business rules over finite histories. We introduce such a BRL and show that it can express many common types of business rules. We introduce two interesting properties of BRL formulas: the future stability and the past stability. The monitor should be able to verify the business rules over the complete history, which is increasing over time. Therefore we consider abstractions of the history. Actually we generate from a set of business rules a labeled transition system (with countable state space) that can be executed by the monitor if each relevant event of the business process triggers a step in the labeled transition system. As long as the monitor is able to execute a step, the business rules are not violated. We show that for a sublanguage of BRL, we can transform the labeled transition system into a colored Petri net such that verification becomes independent of the history length.
AB - Information systems supporting business processes are usually very complex. If we have to ensure that certain business rules are enforced in a business process, it is often easier to design a separate system, called a monitor, that collects the events of the business processes and verifies whether the rules are satisfied or not. This requires a business rule language (BRL) that allows to verify business rules over finite histories. We introduce such a BRL and show that it can express many common types of business rules. We introduce two interesting properties of BRL formulas: the future stability and the past stability. The monitor should be able to verify the business rules over the complete history, which is increasing over time. Therefore we consider abstractions of the history. Actually we generate from a set of business rules a labeled transition system (with countable state space) that can be executed by the monitor if each relevant event of the business process triggers a step in the labeled transition system. As long as the monitor is able to execute a step, the business rules are not violated. We show that for a sublanguage of BRL, we can transform the labeled transition system into a colored Petri net such that verification becomes independent of the history length.
UR - http://www.scopus.com/inward/record.url?scp=78650904547&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-18222-8_7
DO - 10.1007/978-3-642-18222-8_7
M3 - Conference contribution
AN - SCOPUS:78650904547
SN - 9783642182211
VL - 6550 LNCS
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 144
EP - 173
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
T2 - 30th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency
Y2 - 22 June 2009 through 26 June 2009
ER -