Wyniki wyszukiwania - BazTech

1

Refinement of Synchronizable Places with Multi-workflow Nets

Hee K. N. van, Sidorova N., Werff J. M. van der

Fundamenta Informaticae

|

2013

|

Vol. 122, nr 1-2

59--83

EN

Stepwise refinement is a well-known strategy in system modeling. The refinement rules should preserve essential behavioral properties, such as deadlock freedom, boundedness and weak termination. A well-known example is the refinement rule that replaces a safe place of a Petri net with a sound workflow net. In this case a token on the refined place undergoes a procedure that is modeled in detail by the refining workflow net. We generalize this rule to component-based systems, where in the first, high-level, refinement iterations we often encounter in different components places that represent in fact the counterparts of the same procedure “simultaneously” executed by the components. The procedure involves communication between these components. We model such a procedure as a multi-workflow net, which is actually a composition of communicating workflows. Behaviorally correct multi-workflow nets have the weak termination property. The weak termination requirement is also applied to the system being refined. We want to refine selected places in different components with a multi-workflow net in such a way that the weak termination property is preserved through refinements. We introduce the notion of synchronizable places and show that weak termination is preserved under the refinement of places with multiworks if and only if the refined places are synchronizable. We give a method to decide if a given set of places is synchronizable.

2

Generation of Database Transactions with Petri Nets

van Hee K.M., Sidorova N., Voorhoeve M., van der Werf J.M.

Fundamenta Informaticae

|

2009

|

Vol. 93, nr 1-3

171-184

EN

Deleting a record from a database table without modifying other records or tables can easily lead to a violation of the database constraints. The same holds for other database operations. In this paper we generate descriptions of transactions triggered by a given operation, guaranteeing that if the database is in a consistent state before a transaction starts, it will be in a consistent state after it is finished. We describe transactions as models of a special subclass of Coloured Petri nets where token values are vectors of identifiers. This class is powerful enough to model transaction execution and it allows for some formal analysis, like soundness.

3

Working with the Past: Integrating History in Petri Nets

Hee K., Serebrenik A., Sidorova N., Aalst W.

Fundamenta Informaticae

|

2008

|

Vol. 88, nr 3

387-409

EN

Most information systems that are driven by processmodels (e.g., workflowmanagement systems) record events in event logs, also known as transaction logs or audit trails. We consider processes that not only keep track of their history in a log, but also make decisions based on this log. To model such processes we extend the basic Petri net framework with the notion of history and add guards to transitions evaluated on the process history. We show that some classes of historydependent nets can be automatically converted to classical Petri nets for analysis purposes. Some of these classes are characterized by the form of the guards (e.g., LTL+Past guards), while others by restrictions on the underlying classical Petri net.

4

Token History Petri Nets

van Hee K., Serebrenik A., Sidorova N.

Fundamenta Informaticae

|

2008

|

Vol. 85, nr 1-4

219-234

EN

State of the art information system commonly record events in log files, also known as audit trails. Moreover, business processes often go beyond the sole recording the events and base decisions on the events observed in the past. To model such processes we extend the basic Petri net framework with the notion of history by associating tokens with histories, adding guards evaluated on the history to the transitions and mapping arcs to expressions involving histories. Guards and arc expressions can involve data associated with the transitions.

5

Checking Properties of Adaptive Workflow Nets

van Hee K., Oanea O., Serebrenik A., Sidorova N., Voorhoeve M., Lomazova I.A.

Fundamenta Informaticae

|

2007

|

Vol. 79, nr 3-4

347-362

EN

In this paper we consider adaptive workflow nets, a class of nested nets that allows more comfort and expressive power for modeling adaptability and exception handling in workflow nets. We define two important behavioural properties of adaptive workflow nets: soundness and circumspectness. Soundness means that a proper final marking (state) can be reached from any marking which is reachable from the initial marking, and no garbage will be left. Circumspectness means that the upper layer is always ready to handle any exception that can happen in a lower layer. We define a finite state abstraction for adaptive workflow nets and show that soundness and circumspectness can be verified on this abstraction.

6

Resource-Constrained Workflow Nets

van Hee K., Sidorova N., Voorhoeve M.

Fundamenta Informaticae

|

2006

|

Vol. 71, nr 2,3

243-257

EN

We study concurrent processes modelled as workflow Petri nets extended with resource constrains. Resources are durable units that can be neither created nor destroyed: they are claimed during the handling procedure and then released again. Typical kinds of resources are manpower, machinery, computer memory. We define structural criteria based on traps and siphons for the correctness of workflow nets with resource constraints. We also extend the soundness notion for workflow nets to the workflow nets with resource constraints; extra conditions concern the durability of resources. We prove some properties of sound resource-constrained workflow nets