Jump to Content

Invited lecturers

Making Work Flow: On the Application of Petri nets to Business Process Management

Wil van der Aalst (Eindhoven, The Netherlands)

Information technology has changed business processes within and between enterprises. More and more work processes are being conducted under the supervision of information systems that are driven by process models.

Examples are workflow management systems such as Staffware, enterprise resource planning systems such as SAP and Baan, but also include many domain specific systems. It is hard to imagine enterprise information systems that are unaware of the processes taking place.

Although the topic of business process management using information technology has been addressed by consultants and software developers in depth, a more fundamental approach has been missing. Only since the nineties, researchers started to work on the foundations of business process management systems. This paper addresses some of the scientific challenges in business process management. In the spirit of Hilbert's problems, 10 interesting problems for people working on Petri-net theory are posed.

The real-time refinement calculus: A foundation for machine-independent real-time programming

Ian Hayes (University of Queensland, Australia)

The real-time refinement calculus is an extension of the standard refinement calculus in which programs are developed from a pre/post style specification. In addition to adapting standard refinement rules to be valid in the real-time context, specific rules are required for the timing constructs such as delays and deadlines. Because many real-time programs are (conceptually) nonterminating, a further extension is to allow nonterminating iterations.

A real-time specification constrains not only what values should be output, but when they should be output. Hence for a program to implement such a specification, it must guarantee to output values by the specified times. With standard programming languages such guarantees cannot be made without taking into account the timing characteristics of the implementation of the program on a particular machine. To avoid having to consider such details during the refinement process, we have extended our real-time programming language with a deadline command. The deadline command takes no time to execute and always guarantees to meet its deadline; if the deadline has already passed the deadline command is infeasible (miraculous in Dijkstra's terminology).

When such a real-time program is compiled for a particular machine, one needs to ensure that all execution paths leading to a deadline are guaranteed to reach it by its deadline. We consider this checking as part of an extended compilation phase. The addition of the deadline command restores for the real-time language the advantage of machine independence enjoyed by non-real-time programming languages.

Is the die cast for the token game?

Alex Yakovlev (University of Newcastle upon Tyne, UK)

As semiconductor technology strides towards billions of transistors on a single die, problems concerned with deep submicron process features and design productivity call for new approaches in the area of behavioural models. The talk will focus on recent developments and new opportunities for Petri nets in designing asynchronous circuits: (a) model refinements for delay-insensitivity, (b) performance-driven mapping of nets to circuits, (c) synthesis of a good net-based 'backend' in the asynchronous design flow.

Model Validation - A Theoretical Issue?

Jrg Desel (Katholische Univ. Eichstt, Germany)

The analysis and verification of a Petri net model can only yield a valuable result if the model correctly captures the considered system and if the analysed or verified properties reflect the actual requirements. So validation of both nets and specifications of desired properties is a first class task in model-based system development. This contribution investigates validation concepts based on various chapters of Petri net theory.

The Challenge of Object Orientation for the Analysis of Concurrent Systems

Charles Lakos (Uni of Adelaide, Australia)

This talk will review the benefits of object orientation in software development and will examine the extent to which these can be harnessed in the specification and analysis of models in the Petri Net formalism.

Abstract Cyclic Communicating Processes: A Logical View

P.S. Thiagarajan (Madras, India)

Temporal logics have been very successful as tools for specifying and verifying dynamic properties of finite state distributed systems. An intriguing fact is that these logics, in order to be effective, must semantically filter out at least one of the two basic features of the behavior of distributed systems: indeterminacy and concurrency. It seems difficult to come up with effective temporal logics in which both indeterminacy and concurrency are explicitly handled. More precisely, the natural logics that one comes up with turn out to be undecidable in terms of the associated satisfiability problems.

Our goal is to exhibit a new class of 1-safe Petri nets for which the satisfiability problem associated with a powerful monadic second order logic -that handles both indeterminacy and concurrency- is decidable; despite the fact the underlying nets may be quite complex. This class arises by blowing up abstract net systems that correspond to 1-safe colored marked graphs but where the color domains are finite.. The latter objects can be naturally viewed as cyclic processes that manipulate finite data values and communicate by synchronization actions. Such a network of processes often correspond to open systems whose communication patterns are deterministic. A typical example is a ring network where each node interacts with its environment, does an internal computation, talks to its left neighbor, talks to its right neighbor; and this pattern is repeated endlessly. A simple but useful rephrasing of our main result is that the monadic second order theory of abstract cyclic communicating processes is decidable.

 

top^