| System Engineering. A Petri Net Based Approach to Modelling, Verification and Implementation. | 
|
|
| System Engineering. A Petri Net Based Approach to Modelling, Verification and Implementation. |
|
In the past years an increasing demand for precise and graphical modelling techniques has become visible in almost all fields of computer applications from industry, commerce and research. This is due to growing requirements for efficient and reliable methods on the one hand and increased power of computer tools on the other.
It is thus not surprising that Petri nets have become a common technique for the specification, validation and performance evaluation of systems, since they provide an intuitive approach, formal techniques and graphical description methods.
In the introduction (of the summer school) participants will be trained in to all these features, starting from a very basic level up to rather sophisticated skills. This will be possible by means of an integrated approach, combining lectures, classroom exercises and computer sessions with Petri net tools.
The introduction will start with a general and intuitive notion of Petri nets and the general principles behind them. Then, an informal tutorial will introduce the basic models of place/transition nets and high level nets, leading to different formal representations to be used in computer tools. For applications to systems analysis and verification, powerful mathematical methods, like linear programming, will be employed to verify correctness properties like safeness, liveness and reachability.
After the first two days the participant will be prepared to enter the lessons on particular applications.
The phenomenon of workflow management will have a tremendous impact on the next generation of information systems. As the workflow paradigm continues to infiltrate organizations that need to cope with complex administrative processes, the WFMS will become a fundamental building block. Therefore, the subject workflow management is of utmost importance for people involved in the (re)design of administrative processes or the development of systems to support these processes. The Petri net formalism provides a firm theoretical basis for the modeling and analysis of workflow processes. The course addresses the following subjects: workflow management concepts, architecture of workflow management systems, mapping workflow concepts onto Petri nets, organizational modeling, verification, and performance analysis of workflows.
The design and control of Flexible Manufacturing Systems (FMS) is a very complex task: many different elements have to be combined, and many different aspects must be taken into account. This complexity has raised the need of use of formal models in order to represent and validate the system.
Petri nets are a family of models well suited for the domain: easy representation of concurrency and competition relations, application of different desing strategies, ability to generate code in an automatic way, a well defined semantics applicable for the qualitative and quantitative analysis and a nice graphical user interface.
The aim of the course is to show how Petri nets can be used for the modeling and analysis of Flexible Manufacturing Systems (focusing mainly in qualitative aspects).
Formal modelling is a key for verification and evaluation of telecommunication systems. Our application concerns a Multi-Agent System of contract monitoring. The application acts in the context of the electronic market. We use a new object-based formalism, which integrates the principles of the ODP standard. We transform these high-level formalisms into the uniform high level Petri net formalism while retaining the original system semantics. The CPN-AMI tools will support the modelling and the analysis of this application.
Systems will inevitably grow in scale and functionality. Therefore, the likelihood of subtle errors is also increasing. A first goal of system engineering is to take advantage of the investment in modelling to generate a prototype of the system, and to have an implementation consistent with the validated model. A second goal is to provide mathematically based methods and tools for verifying such systems.
There exists a diversity of verification methods developed for Petri nets. This part of the school aims to clarify the bases for choosing an adequate method for each problem, by discussing issues involved in the design and the application of each method: 1) Net models that the method is able to verify; 2) Kinds of properties to check; 3) Families of methods; 4) The interplay of different methods.
Emphasis will be put on the presentation and discussion of a way to produce a distributed application from a Petri Net specification. The produced application is not a Petri net simulation and can be integrated in a complex execution environment.
Efficient methods for the construction of the state space are presented in this tract. Several verification methods working on the state space are analyzed and compared.
The use of the net structure for formal verification of net properties is presented. Structural reduction of nets, linear algebra based techniques, and graph based techniques for net subclasses are the main topics.
In this tract the use of logics for formal verification of net properties is presented. Linear Logic enriched by algebraic specifications leads the way to rewriting logic semantics for algebraic Petri nets. For verification of temporal properties of high-level nets a UNITY-style logic is employed.
CPN-AMI is a Petri Net based CASE environment that will be used in the practical tasks and exercises of the school. It offers a set of services to ease the work of designers who specify a system by means of the Petri net theory and benefit from it. It relies on the Macao graph Editor which also behaves as the User Interface of CPN-AMI. This software tool runs on Sparc/SunOS (4.1.4 or later) Sparc/Solaris (2.4 or later) and UltraSparc/Solaris (2.5.1 or later).
CPN-AMI is a project initiated in 1987 by Professor C.Girault in the team "Systèmes répartis et coopératifs", in the Laboratoire d'Informatiques de Paris 6 (Previously MASI) in the Université Pierre & Marie Curie, Paris (France).
The following tools will be used during the course on Workflow Management Systems to demonstrate the application of Petri-net-based software to this domain and which preferably could be used by the students for doing assignments: