Database Reference
In-Depth Information
interest rate. The calculation of the new interest rate, of course, is also based on the old
interest rate. However, the new interest rate is not available to the other calculations that
occur in the same step.
In the Statechart Analysis section, we will use Algorithm 2 to identify the set of transi-
tions in Figure 10 that may lead to non-confl uence.
Observable Determinism
A transition is
observable
if its action is visible to the environment. A good example
would be “print Profi t” where Profi t is a variable. Consider a set of non-prioritized and ob-
servable transitions that are fi red at the same time. If the order of the output of the system
does not depend on their order of execution, then the set is
observably deterministic
.
Theorem 4.
If a statechart S implements the statemate semantics, then S is observably
deterministic.
Proof:
In the statemate semantics of statecharts, all actual updates of data items (or
variables) are done at the end of a step (Harel & Naamad, 1996). Thus, any values that are
displayed or printed out during the execution of a step are updated at the end of the previ-
ous step. Hence, displaying values to the environment cannot interleave with updating of
values within the system. Therefore, if a system implements the statemate semantics, then
it is observably deterministic.
The next theorem shows the relationship between the properties Observable Determin-
ism and Confl uence.
Theorem 5.
If a statechart S is observably deterministic, then S is confl uent.
Proof:
For each transition in S, we add the action “show the entire current status of
S”. Thus if S is observably deterministic, then the printout of the status of S will be deter-
ministic, which means S is confl uent.
By Theorem 5, if a statechart is not confl uent and its outputs are visible, then it is
not observably deterministic. In the Statechart Analysis section, we will identify the set of
transitions in Figure 10 that may lead to non-observable determinism.
CASE STUDY
We introduce a case study to theoretically validate our algorithms within a real-life
context. Benbasat, Goldstein and Mead (1987) and Yin (1994) endorse the use of case stud-
ies to capture knowledge from practice. Our study generates theory with the assistance of
algorithms. These algorithms prove that statecharts are valuable in determining termination,
confl uence, and observable determinism in workfl ows. Therefore, the results of the algo-
rithms provide validated theory related to workfl ow properties. We also extend our theory
by testing these properties in a real-life context (the case study). The case study approach
offers a vehicle to construct applied theory from scholarly theory.
The case study was with Moore Business Communication Services (BCS), located
in Logan, UT. Since the case study was administered in 1999-2000, Moore BCS has been
recast as Moore Wallace Incorporated (MWI). From this point forward, we will use the
MWI name when we refer to the case. MWI is a large company with approximately 2.32
billion dollars in 2003 revenue. MWI helps large corporations increase their competitive-
