In this paper, Timestamp Petri nets - a special kind of timed Petri nets - and a Logic of Actions are used to specify process requirements. Petri net implementations of such specifications are used for a better visualization and to prove whether a given realization is sound and complete with respect to a given specification. The theory is applied to the specification of workflow processes. An example shows how to prove that a given workflow fulfills time constraints required by the management of a company. A Software Requirements Specification (SRS), as defined in (Davis, 1993), “is a document containing a complete description of what software will do without describing how it will do it”. An SRS is the result of an early phase within a software project and builds the base for the further development. It is a collection of user needs and technical restrictions that must be considered while the software is being built. Because of its central importance, many academic and practical work concentrates on the following problems: Which formal techniques and languages exist to define requirements such that they can be transformed into a formal specification and later on into an implementation? If a given formal requirements definition cannot be transformed into an implementation automatically, is it at least possible to prove whether a realized implementation fulfills this requirement definition? In the following, we concentrate on special requirement definitions - specifications of processes. We use a Logic of Actions proposed in (Simon, 2001a) to formally define process specifications and realizations. Petri net representations of these definitions are used to illustrate the represented processes and for proving given realizations against given specifications within this theory. They will be explained throughout this paper. An example from Workflow Management Systems will be used to illustrate the application of this logic within a software development process. Timestamp Petri Nets (Hanisch, Lautenbach, Simon, and Thieme, 1998) are a special kind of Petri net (Peterson, 1981, Reisig, 1985) allowing the representation time information. Each token of a timestamp net carries a timestamp designating the moment the token was put on its
The edge from place p1 to transition a is permeable from eight to ten, i.e. in interval [5+3; 7+3]. Within this interval, transition a is able to fire any moment. If doing so, the resulting token on place p4 gets a timestamp with value eight to ten dependent on the moment transition a actually fires.
The edge from p2 to b is permeable from ten to eleven and that from p3 to b from nine to twelve. Since both edges are only permeable simultaneously from ten to eleven, transition b is only able to fire within this interval. Afterwards, the resulting token on p5 will carry a token with a timestamp between ten and eleven. [0;1] [1;2] c c <9>
[0;1] <11>
[1;2] p1 p2 p3 <3> <7> <1> [5;7] [3;4] [8;11] p1 p2 p3 [5;7] [3;4] [8;11] a place. Intervals at the incoming edges of transitions specify their permeability with respect to the marking of the adjacent place. If all pre-places of a transition are marked and all its incoming edges are permeable simultaneously, then this transition is able to fire. Figure 1 shows a timestamp net consisting of five places p1, …, p5 and three transitions a, b, and c. Place p1 is marked with a token with timestamp three, the token on p2 has a timestamp seven and the token on p3 has a timestamp of one. Therefore, the token on p2 is the youngest and that on p3 is the eldest shown in the net. All other places of the net are unmarked.
Timewise stuckness always occurs when one incoming edge of a transition looses its permeability before another become permeable at all. Hanisch, Lautenbach, Simon, and Thieme (1998) have presented an analyzing technique that can be used to determine whether certain transitions in a timestamp net might get timewise stuck. The same analyzing technique can be used to determine time parameters within such a net such that certain transitions will never get timewise stuck.
Until now, applications of timestamp nets have been rather technical
In Simon, (2001a), a Logic of Actions (LA) is proposed. Process is the central term in LA. Processes consist of actions which might occur or are forbidden and which are ordered in sequence or might occur coincidentally. Timestamps assigned to actions are used to determine their moment of occurrence. The extension of LA by time is called Timestamp Logic of Actions (TiLA) .
Modules, the formulas of LA and TiLA, are used to specify process sets. Before (<), after (>), coincident (=), forbid (¬), and (∧), xor (+), and iteration operators are used to combine sub modules to complex ones.
[[3;4] a < [[6;7] b + [5;8] c]] is an example for a TiLA module. It specifies processes where action a occurs 3 to 4 time units after process start. Afterwards, either action b occurs after 6 to 7 time units or c occurs after 5 to 8 units of time and the processes end. A Petri net implementation of this module is shown in figure 3.
s [3;4] a [6;7] [5;8] b c [0;∞] g In a Petri net implementation of a module, the same processes can be realized as are specified by the module. A process in such a net is a firing sequence reproducing the empty initial marking and in which the start transition s and the goal transition g, used to specify the beginning and the end of each process, occur exactly once. Actions are represented by equally named transitions. The symbol ∞ designates that the respective edge never looses its permeability after it has been marked as long as the token stays on the adjacent place. Petri nets are not only a means to visualize TiLA modules but rather are used to simplify proving within this theory. The aim of verification within TiLA is to prove whether a given realization of processes fulfills a given process specification. A realization can be proven to be sound and complete with respect to a specification.
M1 fulfills M2 (M1 →→ M2) iff P[CM2(M1)] ⊆ P[CM1(M2)] Within this definition, the operator C is used to mutually complete the modules in order to make them comparable. In all processes of completed modules each action of this module either occurs or is forbidden. M1 fulfills M2, if the set of completed processes realized by M1 is a subset of those specified by M2.
A realization is called sound if it only realizes specified processes. In terms of our logic, it fulfills its specification. If all specified processes are realized then the realization is complete.
Let S be a specification given as a TiLA module over a set of actions A, and R a realization also given as a TiLA module over the same set of actions A.: • •
This definition of sound and complete is based on counting the processes specified by modules. However, in the case of TiLA modules the number of specified processes is infinitely large. Therefore, we will consider an alternative approach to proving in the following section.
Instead of comparing the process sets of a specification S and a realization R, we do verification by conjoining S and R and determining whether this rules out processes specified by R. In this case, R defines processes not specified by S and therefore R does not fulfill S.
M1 →→
M2 ⇔ P[M1 ∧ M2] = P[CM2(M1)] We use theorem 2 instead, if undesirable behavior is specified instead of desired behavior, i.e. if ¬S and not S is given.
M1 →→
M2 ⇔ |P[M1 ∧ ¬M2]| = 0
Both theorems have been proven in
For given Petri net implementations of modules M1 and M2, we can realize M1 ∧ M2 by joining (×) the completed implementations N (CM2(M1)) and N (CM1(M2)). Joining identifies equally named transitions of both participating nets (including s and g) and fuses them. All places of the participating nets also occur in the result of the join except those which cause redundant structures. Additionally, places are added to prevent transitions representing a certain action and others representing its prohibition from occurring both in processes.
and a realization
The effect of joining Petri net implementations of modules is that the resulting net realizes
only such processes specified by each participating module or its Petri net implementation,
respectively. The completion step is responsible for making the participated processes
comparable. This observation leads to the following theorem that is central in
N (CM2(M1)) × N (CM1(M2)) implements M1 ∧ M2
S = [[3;4] a < [[6;7] b + [5;8] c]]
R = [[[4;4] a < [6;7] c] ∧ [0; ¥]¬b].
Specification S describes processes where a occurs three to four units of time after process start. Afterwards, either b occurs six to seven units of time later, or c occurs five to eight units of time later. Realization R describes processes where a occurs exactly after four units of time after process start. Six to seven units of time later, c occurs. In addition, b is forbidden. For proving whether R fulfills S, we first have to mutually complete their implementations. Figure 5 shows this step with respect to the implementation of R. Although the result of this completion looks quite complex this is only a problem of visualization. The operation itself is linear dependent on the number of transitions in the net.
s s As we mentioned above, completion is responsible for making the process sets of modules comparable. Therefore, this completion step, as demonstrated above, is also important on the Petri net level (cf. Simon, 2002). However, in Petri net implementations we can make an observation that simplifies further calculations: Processes of such a Petri net implementation are firing sequences reproducing the empty initial marking. Thus, only such firing sequences can be realized which are also realizable in the same Petri net without time information. In such a Petri net without time information, such firing sequences reproducing the empty initial marking must be covered by T-invariants. Therefore, each transition that is not included in any T-invariant cannot occur in any realizable process of such a Petri net implementation. In other words: the corresponding action does not occur or is forbidden in any process of the implemented completed module.
If we consider the Petri net in figure 5 without time information, we only find one T-invariant covering transitions s, a, ¬b, c, and g. No one of the transitions added throughout the completion step is participated in any process. Therefore, we can immediately role back our completion step and can conclude that in our realization already each specified process must have been complete.
Completing the Petri net implementation of the specification S and reducing this result with the aid of the T-invariant method described above results in the implementation shown in figure 6.
s [3;4]
a Figure 7 shows the result of joining these intermediary results. s s s [4;4] Comparable to our reductions of the completed modules, we can also simplify this result using the T-invariant method. This time, we can rule out transitions ¬a, b, and ¬c from occurring in any process. This leads to the Petri net implementation of S ∧ R as shown in figure 8. In all firing sequences beginning with start transition s, both pre-places of transition a get marked at the same moment. Three to four time units later the first incoming edge of a is permeable. The second one is permeable exactly after four time units. Since transition a can only fire if all its incoming edges are permeable simultaneously, the permeability of both edges results from the intersection of interval [3;4] and [4;4]. As a result, we get the net shown in figure 9. In the same way we can proceed with the incoming edges of transition c. The result is the Petri net implementation of our realization R as shown in figure 4. With the aid of theorems 1 and 3 we conclude that the realization fulfills the specification.
In the following sections, we show an application of this theory to the field of Workflow
The development of Workflow Management Systems
The expression workflow is used to describe human work and the basic terms on this area are
defined by the Workflow Management Coalition (WfMC). A workflow is "the automation of a
business process, in whole or part, during which documents, information or tasks are passed
from one participant to another for action, according to a set of procedural rules". A
Workflow Management System "defines, creates and manages the execution of workflows
through the use of software, running on one or more workflow engines, which is able to
interpret the process definition, interact with workflow participants and, where required,
invoke the use of IT tools and applications"
These fundamental definitions by the WfMC highlight the most important parts of workflow systems from the point of view of automation: • •
attributes, qualifications and/or skills"
(i.e. what is intended to happen) is defined in a is managed by a
(a represenation of what is intended to happen)
(controls automated aspects of the business process) Sub
composed of used to create & manage via which may be
or
(which are not managed as part of the Workflow System)
Activities during execution are represented by
Process Instances (a representation of what is actually happening) include one or more which include
and/or
(tasks allocated to a workflow participant)
(computer tools/ applications used to support an activity) Obviously, processes are central in the definition of Workflow Management Systems. They are detailed in nature because they cover both, the usual business process as well as exceptions from this process in the case of faults. However, a first specification of such a business process might come along without such details. In the following section we consider the question how to prove whether a workflow definition fulfills such a previously made specification.
In the following, we use TiLA to answer the question: Is every process of a complex
realization conforming a given specification?
To demonstrate this, we consider an exemplary workflow described in
[[0] r < [[0] cc ∧ [0] cd] < [0] c < [0] a < [[0] p + [0] sl] < [0] f] We abbreviate intervals specifying a single moment like [15;15] by [15]. Figure 12 shows a Petri net implementation of this module.
[10] [15] cc cd [0;∞] c [0;∞] [10] [25] p sl [0] r [20] a [0] f [0;∞] g As one can imagine, the module only specifies a very simple workflow. However, for a manager of an insurance company this already might be too complex. S/he might mostly be interested in the maximal duration of the entire process. A typical question s/he could ask for is: Does it take no longer than 55 units of time after process start until all process data and all used documents are filed? In the Logic of Action, the formulation of this question is rather simple. [[55] f] is a specification of the question. Figure 13 shows the implementation of this module. For verifying whether our business process fulfills this specification, we join the implementations of both modules. Figure 14 shows the result of this join. s p1 [0]
r p6
[15] p5 [10]
p7 cc cd [0;∞]
] [0;∞
g [0;∞] Now we have to examine whether the net in figure 14 represents the same processes as the net in figure 12. If it represents less, this can only be caused by transition f getting timewise stuck.
Firing transition s produces tokens with timestamp α on p1, p2, p3, and p4. After firing transition r, places p2, p3, p4, p5, and p6 are marked. The tokens on p2, p3, and p4 have timestamp α, those on p5 and p6 have timestamp β = α + 0 = α. By firing cc and cd, places p5 and p6 get unmarked, p7 gets a token with timestamp γ = β + 10 = α + 10, and p8 gets a token with timestamp δ = β + 15 = α + 15. The tokens on places p2, p3, and p4 still have timestamp α. Assuming transition c fires as soon as possible, p7 and p8 get unmarked and p9 gets a token with timestamp ε = min{γ, δ} = α + 15. Firing transition a causes a marking where p10 has a token with timestamp ζ = ε + 20 = α + 35, and where p2, p3, and p4 are still marked by tokens with timestamp α. Now, we have the possibility either to fire transition p or to fire transition sl.
• •
Firing transition p marks p11 and p12 by tokens with timestamp θ = ζ + 10 = α + 45.
afterwards by firing g.
Firing transition sl marks p12 and p13 by tokens with timestamp λ = ζ + 25 = α + 60.
incoming edge of f (from place p4 to f) has already lost its permeability. Therefore, transition f is timewise stuck and the process cannot be finished.
Consequently, the realization of our business process does not fulfill the manager’s specification. Moreover, we observe that we have to optimize our business process such that it is 5 units of time faster. This can be achieved by optimizing action contact department, assess, or send letter.
In this paper, we have used a Logic of Actions to specify process requirements. Petri net implementations of the formulas of our logic are used for visualization and for proving. As an application, we chose the verification of workflows. We demonstrated our approach with the aid of an example.
Our models and proving techniques are rather formal. As a consequence, they allow precise descriptions of the systems under examination. However, especially in a business environment these descriptions must be substituted by less formal ones, i.e. our mathematical methodology must be hidden from a possible user. Our future work will focus on this problem.