-
Data flow analysis has shown to be a utility for business process modeling
and analysis, be it for supporting formal verification [
5,6
], for analyzing
dataor control-flow related process properties [
2,11
], or for optimization and
reengineering [
8
]. In particular two aspects make it such a useful method: (1) Data
lfow analysis provides a general framework which can be easily adjusted to
new domains and analysis problems, (2) data flow analysis is grounded on
wellfounded theories like Kildall’s lattice-theoretic formulation [
7
] or Cousot’s abstract
interpretation [
4
]. While the latter aspect ofers a way to formally show an analysis
to be correct, until now, only a small number of data flow analyses for business
processes have been proven correct, mostly using pencil-and-paper proofs and just
considering termination [
2,5
]. This is suprising considering the recent advances
made in the verification of static analysis. State-of-the-art approaches define
not only an analysis but rather add a mechanized, that is machine-checkable
proof of its correctness. The term certified analysis has therefore been coined, as
a user does not need to trust in such an analysis but can automatically check
its conjoined correctness proof. Most notably, the verification of an optimizing
C compiler [
9
] documented the power of the certified analysis approach.
In this position paper, we argue for the idea of a certified analysis of business
processes. We believe the advantages to be manifold. For instance, the complexity
of business process modeling languages like BPEL and BPMN make not only
the design and implementation of processes, but also of analyses error-prone. An
approach for proving analysis correctness thus helps in regaining confidence. This
can be of vital importance considering, e.g., business processes in healthcare.
Further, a mechanized correctness proof of a compliance analysis augments
process auditing scenarios [
1
] with an orthogonal check that the audit itself can
be trusted. Synthesizing an analysis from its correctness proof, even relieves
the analysis designer from the implementation burden. In the following, we will
introduce the concept of certified analysis based upon abstract interpretation,
sketch challenges which arise when applied to business processes and finally
outline our first steps towards a certified data flow analysis of business processes.
Data flow analysis can be seen as abstract interpretation [
4
], where programs are
evaluated using abstract values instead of concrete values. As an example, instead
of performing arithmetic operations on integers when executing a program, an
analysis may only track whether an integer has abstract value odd or even. In this
way, e.g., addition boils down to four cases: even +even = even, even +odd = odd,
odd + even = odd, and odd + odd = even. The domains of abstract and concrete
values are connected by the concretization function γ , which maps abstract values
to the represented concrete ones, e.g., γ (odd) = { 1, 3, 5, . . . } . In addition, the
abstract domain A should form a partially-ordered set, reflecting precision among
abstract values such that ∀ a, b ∈ A : a ≤ b ↔ γ (a) ⊆ γ (b), and contain a distinct
top element with ∀ a ∈ A : a ≤ top, representing all concrete values. Executing a
program’s statements on concrete values can be formalized using Hoare’s weakest
precondition calculus, as in [
3
], which yields the concrete semantics. The efect of
statements on abstract values is denfied by the analysis in terms of a monotone
function f : A → A mimicing, e.g., above’s addition example, which in this way
provides the abstract semantics. An analysis based upon abstract interpretation
then calculates a fixpoint abstract value, i.e., f (a) = a, for a given program by
continuously applying the abstract semantics to an initial abstract value until the
ifxpoint is reached (optionally using accelerators like widening/narrowing [
4
]).
An analysis can then be shown correct based upon abstract interpretation, if:
∀ a ∈ A : cinitial ∈ γ (a) →
f (a) = a → ∀
c′ : cinitial ⇝ c′ →
c′ ∈ γ (a)
meaning that a fixpoint a of the abstract semantics, that includes the initial
concrete value cinitial of the program in its concretization, also includes the concrete
values c′ of all reachable program states, cinitial ⇝ c′, in its concretization. Note
that correctness here refers to soundness, i.e., the abstract value a is guaranteed
to (over-)approximate the concrete value. The Coq proof assistent1 has been
shown of use for proving analysis correctness [
3,9
]. Its inductive types provide a
way for encoding programs and its recursive functions for encoding concrete and
abstract semantics. Proving analysis correctness in Coq may still require manual
work, yet Coq allows for automatic proof validation and even to synthesize the
analysis implementation1, which justifies the notion of a certified analysis .
3
Research Challenges and First Steps
While the automated analysis for certifying business processes has been a recent
research topic [
1
], we are not aware of any prior work on the certification of such
an analysis for business processes itself. As indicated above, though, the area of
static program analysis provides a rich spectrum of methods for proving analysis
correctness. Yet, business processes and business process modeling languages
feature certain peculiarities which challenge a certified analysis approach:
1 https://coq.inria.fr/ (link was last followed on February 1, 2017)
– First, as parallelism is essential to business processes, the concrete and
abstract semantics need to reflect parallel executions. Application of
(concurrent) separation logic [
10
] can thus be of advantage, extending the Hoare
calculus with a rule for independently reasoning about parallel processes.
– Second, the phletora of language constructs in languages like BPEL or BPMN
make formalizing the concrete semantics a tedious task. We thus opt for an
approach, where we consider a kernel of basic language constructs, mapping
all other constructs onto the kernel. This is a common method to boil down
the complexity of a language [
2
] and furthermore provides a starting point
for coping with the diferent and often mixed types of data oflw definitions
(XPath, Java, scripting languages, etc.) used in BPMN processes.
– Third, unstructured processes. While unstructuredness in case of sequential
control flow alone can be handled by basing semantics on low-level jump
operations instead of high-level ifelse or loop statements, mixed use of gateways
as possible in BPMN, even more in the presence of the notoriously dificult
to formalize (inclusive) OR gateway, provides for a real research challenge.
Currently, we are formalizing a toy language for business processes in Coq,
supporting basic workflow patterns, e.g, sequence, parallel split/synchronize,
exclusive choice/merge, and a data flow analysis for computing communication
dependencies (see [
2
]). This language shall be enriched in future steps. Future
work will also address other analyses, where we want to follow a modular approach
using a general analysis framework, which is instantiated for a specific analysis.