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
- visualize the the behaviour
- simulate the bahaviour
- analyse the behaviour
- verify system properties
- construct a controller
- find fauls
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:
The Component Tools is currently implemented by a group of student in their
one year project: Projektgruppe:
Infrastruktur zur Konstruktion, Analyse und Validierung
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.
Event Driven Process Chains (EPCs) are a widely used notation for modelling
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
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.
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
More detailed information on MCiE can be found at
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:
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
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:
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: