Campus Event Calendar
Event Entry
What and Who
Reasoning with Data-Centric Business Processes
Peter Baumgartner
NICTA
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 3 July 2012
14:30
60 Minutes
E1 4
024
Saarbrücken
Abstract
Andreas Bauer, Peter Baumgartner and Michael Norrish
NICTA and ANU
We describe a novel approach to modelling and reasoning about data-centric business
processes. We model business processes in terms of smaller fragments, whose
possible interactions are constrained by first-order logic formulae. In turn,
process fragments are connected graphs annotated with instructions to modify
data. Correctness properties concerning the evolution of data with respect to
processes can be stated in a first-order branching-time logic over built-in
theories, such as linear integer arithmetic, records and arrays.
We are currently developing reasoning methods for analysing the business
process models above wrt their correctness properties. More specifically, we
distinguish between two kinds of model checking problems, depending on whether
the initial state is specified in full, or not. The latter case requires
reasoning on only partially given input data and is considerably harder. To
this end, we present a tableau procedure that reduces these (bounded) model
checking problems to first-order logic over arithmetic. The resulting proof
obligations are suitable to be passed on to appropriate ``off-the-shelf''
theorem provers.
In the talk, we detail our modelling approach, describe the reasoning
components and report on first experiments.
NICTA and ANU
We describe a novel approach to modelling and reasoning about data-centric business
processes. We model business processes in terms of smaller fragments, whose
possible interactions are constrained by first-order logic formulae. In turn,
process fragments are connected graphs annotated with instructions to modify
data. Correctness properties concerning the evolution of data with respect to
processes can be stated in a first-order branching-time logic over built-in
theories, such as linear integer arithmetic, records and arrays.
We are currently developing reasoning methods for analysing the business
process models above wrt their correctness properties. More specifically, we
distinguish between two kinds of model checking problems, depending on whether
the initial state is specified in full, or not. The latter case requires
reasoning on only partially given input data and is considerably harder. To
this end, we present a tableau procedure that reduces these (bounded) model
checking problems to first-order logic over arithmetic. The resulting proof
obligations are suitable to be passed on to appropriate ``off-the-shelf''
theorem provers.
In the talk, we detail our modelling approach, describe the reasoning
components and report on first experiments.
Contact
Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 06/28/2012 15:46 -- Created document.