Component Tools

Component Tools is a project that supports the modelling, analyis, validation, and verification, and set-up of production systems. The system will be constructed from components. For each component, there will be various models of their dynamic behaviour on different levels of abstraction, of possible faults, of their physical shape and of some other properties. These models will be combined in various ways in order to All this is current research. Some concepts for defining and using component libraries and a first implementation of a tool were developed by Joel Greenyer in his bachelor thesis.

A prototype of the visualization tool, PNVis, has also already been implemented. PNVis is an application for the Petri Net Kernel for the 3D-visualization of Petri net models. You will find more information on PNVis and can download it from the following web page: http://www.upb.de/cs/kindler/research/PNVis.

The Component Tools is currently implemented by a group of student in their one year project: Projektgruppe: Infrastruktur zur Konstruktion, Analyse und Validierung komponentenbasierter Systeme.

AMFIBIA: A Meta-model For the Integration of BusIness process modelling Aspects

There is much work on ontologies, meta-models, and interchange formats for business process modelling. The problem, however, is that most of this work is focused on a particular fomalism, is restricted to some particular aspects, or does not cover all phases from business process modelling to workflow management.

The AMFIBIA project aims at an ontology and a meta-model for all concepts in business process modelling. The ontology should capture the basic aspects of business processes and should be open for adding further aspects. Moreover, the ontology should not be biased towards any aspect or towards any formalism. In particular, it should be possible to map different formalisms to this ontology and to integrate different formalisms by the help of this ontology.

For more information see http://www.upb.de/cs/kindler/research/AMFIBIA.

EPC Tools

Event Driven Process Chains (EPCs) are a widely used notation for modelling business processes. Unfortunately, there are some theoretical as well as some practical problems with the semantics of EPCs. These problems arise from the non-local semantics of some of its constructs. We have investigated this problem, came up with a solution, and are currently implementing a simulator based on the resulting semantics. The next step will be analysis and verification tools for EPCs based on this semantics.

EPC Tools is an extensible eclipse-based tool suite that supports editing, simulating, analysing, and verifiying business processes modelled as EPCs. It will support the interchange format EPML, which in turn, supports tranformations to several widely-used other tools.

More details on EPC Tools and possibilities for downloading EPC Tools can be found at http://www.upb.de/cs/kindler/research/EPCTools.

MCiE

The idea of the Model Checking in Education (MCiE) project is to supplement a course on model checking with an exemplary implementation in Java. It is not meant to be the most efficient implementation (how could in be in Java), but a clean, understandable and safe implementation.

More detailed information on MCiE can be found at http://www.upb.de/cs/kindler/Lehre/MCiE.

DAWN

DAWN is a technique for specifying, modelling, and verifying distributed algorithms (Distributed Algorithms Working Notation). DAWN is tuned to the verification of network algorithms for classes of networks; i.e. it supports parameterized verification. It combines concepts from Petri net theory and from temporal logic.
More detailed information on DAWN can be found at Humboldt-University: http://www2.informatik.hu-berlin.de/top/forschung/archiv/vertalg/dawn/index.html.

Scenarios

With the advent of UML, sequence diagrams and message sequence charts (MSCs) are commonly used for specifying software. Sequence diagrams are particularly suited for the specification of the interaction of independent components. We subsume all variations of these techniques under the general term scenario.
In this project we develop notations and proof techniques that support the use of scenarios. The semantics must reflect the informal and incomplete character of scenarios. Still, there should be a precise semantics in order to do verification.
Experiences with similar techniques for specifying and verifying consistency protocols show that this approach is feasible.

PNK and PNML

The Petri Net Kernel (PNK) is an infrastructure for implementing Petri net tools. It provides interfaces for the combination of functions and applications on Petri nets. It saves the programmer from implementing standard functionality over and over again. One of the main features of the Petri Net Kernel is its genericity, i.e. it allows the programmer to define his own Petri net types. More detailed information on the Petri Net Kernel can be found at the PNK home page: http://www.informatik.hu-berlin.de/top/pnk/

During the development of the Petri Net Kernel, the need of a type and tool independent interchange format for Petri nets has occurred. Therefore, we started to develop an XML-based interchange format for Petri nets: the Petri Net Markup Language (PNML). More detailed information on PNML can be found at the PNML home page: http://www.informatik.hu-berlin.de/top/pnml/