Papers (Bernd Grahlmann)
-
AMAST'98 (Algebraic Methodology and Software Technology,
Manaus - Brazil, 98):
- Author: Bernd Grahlmann
Abstract:
The PEP tool can be considered to be one of the most widely distributed
Petri net based tools. A continuously increasing functionality and an
adequate graphical user interface may have been good reasons for its
acceptance. Currently the tool contains approximately 500,000 lines of
source code, and supports (to the best of our knowledge) the widest
variety of input formalisms and verification methods of all verification
tools. We briefly review the most recent developments.
Ftp-able versions of the tool and PEP related papers are available
via http://theoretica.informatik.uni-oldenburg.de/~pep.
Keywords:
3D visualisation, C code generation, Parallel programs,
PEP, Petri nets, SDL, Simulation, Verification.
-
SPIN Workshop (Paris 1998):
- Authors: Bernd Grahlmann and Carola Pohl
Abstract:
This paper describes how the PEP tool (Programming Environmnet based on
Petri nets) profits from an integration of the Spin (Simple PROMELA
INterpreter) verification package.
Translation methods from three input formalisms (parallel programs,
high-level and low-level Petri nets) into PROMELA (PROtocol MEta LAnguage)
are discussed and the Spin based verification is compared with a
Petri net based partial order model checker using a number of typical
examples.
Keywords:
Parallel programs, PEP, Petri nets, PROMELA, SDL, Spin,
Verification.
-
ATPN'98 (Application and Theory of Petri Nets - Lisboa 98):
- Authors: Hans Fleischhack and Bernd Grahlmann
Abstract:
In this paper a compositional high-level Petri net semantics for SDL
(Specification and Description Language) is presented. Emphasis is
laid on the modelling of dynamic creation and termination of processes
and of procedures - features, which are, for instance, essential
for typical client-server systems.
In a preliminary paper we have already shown that we are able to use
`state of the art' verification techniques by basing our approach
on M-nets (an algebra of high-level Petri nets). Therefore, this
paper concentrates on the details of the semantics.
A distinctive feature of the presented solution is that the `infinite case'
(infinitely many concurrent process and procedure instances as well
as unbounded capacities of input queues and channels) is covered.
Keywords:
ARQ protocol, Compositionality, Concurrency, Dynamic Processes,
Infinity, Petri Net Semantics, Procedures, SDL.
-
TACAS'98 (Tools and Algorithms for the Construction and Analysis of Systems - Lisboa 98):
- Author: Bernd Grahlmann
Abstract:
This paper introduces a method to combine finite automata, parallel
programs and SDL (Specification and Description Language) specifications.
We base our approach on M-nets exploiting the rich set of composition
operators available in this algebra of high-level Petri nets. In order
to be able to combine different modelling techniques, we rely on
compatible interfaces. Therefore,
- we extend an existing semantics, namely the M-net semantics for the
parallel programming language B(PN)^2; and
- we present an M-net semantics for finite automata.
Considering the hybrid modelling of an ARQ (Automatic Repeat reQuest)
protocol, we show how the different formalisms fit together as well
as the resulting verification possibilities. As a side-effect we
describe on-going development of the PEP tool (Programming Environment
based on Petri Nets). As a consequence of our approach we are introducing
a hierarchical `programming with nets' method which is currently
implemented in the high-level Petri net editor of the tool.
Keywords:
B(PN)^2, Finite automata, Hybrid system design, M-nets,
Parallel programs, PEP, Petri nets, SDL, Verification.
-
HICSS'98 (31st Hawaii International Conference on System Science):
Towards Compositional Verification of SDL Systems
An extended but preliminary version is online available
here
- Authors: Hans Fleischhack and Bernd Grahlmann
Abstract:
In this paper, a new method for proving qualitative properties
of SDL-systems is presented, which is based on a compositional
high-level Petri net semantics for SDL. Since emphasis is laid
on the modelling of dynamic creation and termination of processes
and of procedures, our method is especially interesting for
typical client-server systems.
By using M-nets as the semantic model we are able to use
`state of the art' verification techniques. For instance, the
verification component of the PEP tool may be applied which
presently includes partial order based model checking and
algorithms based on linear programming as well as interfaces to
other verification packages such as INA, SMV and SPIN providing
reduction algorithms based on BDDs, on the stubborn set or sleep
set method, and on symmetries.
We show the benefits of our method applying it to a typical
client-server system. After describing how safety, liveness and
progress properties can be checked fully automatically, we give
examples how the compositional nature of the M-net semantics can
be used to solve the `state explosion' problem, and how interactive
verification may extend the verification possibilities.
Keywords:
Compositionality, Concurrency, Dynamic Processes,
Petri Net Semantics, Procedures, SDL, Verification.
-
SDL (Technical Report):
This is a preliminary but extended version of two papers which has
the reference:
The details of the final versions can be found
here and
here.
- Authors: Hans Fleischhack and Bernd Grahlmann
Abstract:
In this paper a high-level Petri net semantics for SDL (Specification
and Description Language) is presented. Emphasis is laid on the modelling
of dynamic creation and termination of processes and of procedures
- features, which are, for instance, essential for typical client-server systems.
In addition to presenting the main ideas as well as the details of the
semantics, we show that we are able to use `state of the art' verification
techniques by basing our approach on M-nets (an algebra of high-level
Petri nets). Therefore, we verify our running example, an ARQ (Automatic
Repeat reQuest) communication protocol, using the verification component
of the PEP tool which presently includes partial order based model checking
and algorithms based on linear programming as well as interfaces to
other verification packages such as INA, SMV and SPIN providing reduction
algorithms based on BDDs, on the stubborn set or sleep set method, and on
symmetries. Moreover, we give examples how the compositional nature of
the M-net semantics can be used to solve the `state explosion' problem, and
how interactive verification may extend the verification possibilities.
Keywords:
ARQ protocol, Compositionality, Concurrency, Dynamic Processes,
PEP tool, Petri Net Semantics, Procedures, SDL, Verification.
-
ATPN'97 (Application and Theory of Petri Nets - Toulouse 97):
- Author: Bernd Grahlmann
Abstract:
The PEP tool is a Programming Environment
based on Petri Nets.
Comprehensive modelling, compilation, simulation and verification
components are embedded in a user-friendly graphical interface.
The basic idea is that the modelling component allows
the user to design parallel systems by parallel finite automata,
parallel programs, process algebra terms, high-level or low-level Petri nets,
and that the PEP system
then automatically generates Petri nets from such models
in order to use Petri net theory for simulation and
verification purposes.
This paper describes the typical usage of the PEP tool by considering
the design of the well-known `alternating-bit' protocol.
Among others, the usefulness of new concepts for the handling
of hierarchies and synchronous communication is explained.
PEP has been implemented on Solaris 2.x, Sun OS 4.1.x and Linux.
Ftp-able versions are available via
http://www.informatik.uni-hildesheim.de/~pep.
Keywords:
`Alternating bit' protocol, B(PN)^2, Hierarchical Petri nets, M-nets,
Parallel finite automata, Parallel programs, PEP, Simulation, Tool,
Verification.
-
CAV'97 (Computer Aided Verification - Haifa 97):
- Author: Bernd Grahlmann
Abstract:
The PEP tool embeds
sophisticated programming and verification
components in a user-friendly graphical interface.
The basic idea is that the programming component allows
the user to design concurrent algorithms in an
imperative language, and that the PEP system
then generates Petri nets from such programs
in order to use Petri net theory for simulation and
verification purposes.
A key feature is flexibility; its modular design eases the
task of adding new interfaces to other verification packages, such as
`INA', `PROD' or `SMV'.
PEP has been implemented on Solaris 2.x, Sun OS 4.1.x and Linux.
Ftp-able versions are available via
http://www.informatik.uni-hildesheim.de/~pep.
Keywords:
Binary decision diagrams, B(PN)^2, Model checking, PEP, Petri nets, Simulation,
Stubborn sets, Temporal logic, Tool.
-
PDSE'97 (Parallel and Distributed Software Engineering - Boston 97):
A Petri Net Semantics for B(PN)^2 with Procedures
An extended but preliminary version is online available
here
- Authors: Hans Fleischhack and Bernd Grahlmann
Abstract:
Verification of parallel programs is a very important goal on the
way to improve the reliability of software. The PEP tool, a Programming
Environment based on Petri nets, allows verification of parallel
programs by a variety of different verification methods (e.g., partial
order or BDD based model checking, and stubborn set or symmetrically
reduced state space analysis) based on a compositional denotational
Petri net semantics.
The main contribution of this paper consists in the development of a
fully compositional high-level Petri net semantics for concurrent
programs with procedures, covering recursion, global variables, and
different types of parameter passing (including call-by-reference).
The semantics (which is already implemented) is oriented towards
verification, i.e., the semantic models are minimised.
Due to the abstract and flexible nature of the Petri net model used, our
approach is very general and may also be applied to other specification
and programming languages. We are, for instance, presently approaching SDL
(Specification and Description Language).
Keywords:
B(PN)^2, High-level Petri Nets, M-nets, Parallel Programming Language,
PEP, Petri Net Semantics, Procedures, Verification.
-
TACAS'97 (Tools and Algorithms for the Construction and Analysis of Systems - Enschede 97):
- Author: Bernd Grahlmann
Abstract:
The PEP tool is a Programming Environment based on
Petri Nets. Sophisticated programming and verification
components are embedded in a user-friendly graphical
interface. The basic idea is that the programming
component allows the user to design concurrent
algorithms in an easy-to-use imperative language, and
that the PEP system then generates Petri nets from such
programs in order to use Petri net theory for simulation
and verification purposes.
The main focus of this paper is the reference component
which represents the bridge between these two worlds.
We integrate references in the formal semantics and
present some of the provided features. Among others the
simulation of a parallel program can be triggered through
the simulation of a Petri net. Program formulae can be
transformed automatically into net formulae which can
then be an input for the verification component.
PEP has been implemented on Solaris 2.x, Sun OS 4.1.x
and Linux. Ftp-able versions are available via
www.informatik.uni-hildesheim.de/~pep.
Keywords:
B(PN)^2, Model checking, Parallel finite automata,
PEP, Petri nets, Reference component, Simulation,
Temporal logic, Tool.
-
(December 96):
This is a preliminary but extended version.
The reference for the final version is:
- Authors: Hans Fleischhack and Bernd Grahlmann
Abstract:
Verification of parallel programs is a very important goal
on the way to improve the reliability of software.
The PEP tool, a Programming Environment based on Petri nets,
allows verification of parallel programs by partial order
model checking based on a compositional denotational Petri
net semantics.
The language supported by the PEP tool covers block structuring,
parallel and sequential composition, choice, iteration, synchronous and
asynchronous communication, including use of unbounded buffers.
At present, it does not cover, however, the
structuring of programs by procedures.
The main contribution of this paper consists in the development
of a fully compositional high-level Petri net semantics for
concurrent programs with procedures, covering recursion, global
variables, and different types of parameter passing (including
call-by-reference).
The semantics will guarantee that the
semantical model (high-level as well as low-level net) of program P is finite
whenever:
- P has only finite data types.
- For each procedure in P only finitely many instances can
be active concurrently.
Due to the abstract and flexible nature of the Petri net model
used, our approach is very general and may also be applied to
other specification and programming languages.
This has already partially been done for SDL
(Specification and Description Language).
Keywords: B(PN)^2, high-level Petri nets, M-nets, parallel
programming language, PEP, Petri net semantics,
procedures, verification.
-
AWPN'96 (3. Workshop Algorithmen und Werkzeuge für Petrinetze - Karlsruhe 96):
- Author: Bernd Grahlmann
Abstract:
The main intention of this paper is to encourage discussion
about standards for Petri net file formats.
We present criteria for good formats and estimate their
significance for different classes of involved persons.
The following persons are considered:
- the designer of a Petri net tool who should integrate analysis algorithms
and editors implemented by different persons at different locations;
- the programmer of an analysis algorithm or a net editor, and
- a user who wants to edit or analyse nets.
The PEP file format serves as an example to explain
design decisions.
Keywords: File Formats, PEP, Petri Nets, Standards.
-
Technical Report (July 96):
This is a preliminary version with reference:
The reference for the final version is:
- Authors: Hans Fleischhack and Bernd Grahlmann
Abstract:
Verification of parallel programs is a very important goal
on the way to improve the reliability of software. The PEP
tool, a Programming Environment based on Petri nets,
allows verification of parallel programs by partial order
model checking based on a compositional denotational Petri
net semantics.
The language supported by the PEP tool covers block
structuring, parallel and sequential composition, choice,
iteration, synchronous and asynchronous communication,
including use of unbounded buffers. At present, it does
not cover, however, the structuring of programs by
procedures.
The main contribution of this paper consists in the
development of a fully compositional high level Petri
net semantics for concurrent programs with procedures, covering
recursion, global variables, and many types of parameter
passing (including call-by-reference).
The semantics will guarantee that the semantical model
of program P is finite whenever:
- P has only finite data types.
- For each procedure in P only a finitely many instances can
be active concurrently.
Due to the abstract and flexible nature of the Petri net
model used, our approach is very general and may also be applied
to other specification and programming languages. This has
already (partially) been done for the Specification and
Description Language (SDL).
Keywords: B(PN)^2, high-level Petri nets, M-nets, parallel
programming language, PEP, Petri net semantics,
procedures, verification.
-
TACAS'96 (Tools and Algorithms for the Construction and Analysis of Systems - Passau 96):
- Authors: Bernd Grahlmann and Eike Best
Abstract:
This paper presents the syntax of a concurrent programming
The PEP system (Programming Environment based on Petri Nets)
supports the most important tasks of a good net tool, including
HL and LL net editing and comfortable simulation facilities.
In addition, these features are embedded in sophisticated
programming and verification components.
The programming component allows the user to design concurrent
algorithms in an easy-to-use imperative language, and the PEP
system then generates Petri nets from such programs. The PEP
tool's comprehensive verification components allow a large range
of properties of parallel systems to be checked efficiently on
either programs or their corresponding nets. This includes
user-defined properties specified by temporal logic formulae
as well as specific properties for which dedicated algorithms
are available.
PEP has been implemented on Solaris 2.4, SunOS 4.1.3 and Linux.
Ftp-able versions are available.
Keywords:
B(PN)^2, Model checking, Parallel finite automata, PEP,
Petri nets, Process algebra, Temporal logic, Tool.
-
RELECTRONIC'95 (9th Symposium on Quality and Reliability in Electronics - Budapest):
- Author: Bernd Grahlmann
Abstract:
Nowadays telecommunication services become more and more complex.
Because of the increasing comfort of these services the
design and especially the verification of the
underlying protocols is an extremely difficult task.
In general protocols are only extensively tested
but not verified due to the lack of powerful tools.
Within the PEP project a tool
has been developed which is well suited to
design telecommunication protocols with a parallel specification
and programming language called B(PN)^2.
Furthermore the automatic translation into
Petri nets allows the efficient verification of various interesting
properties by use of a partial order based model checking algorithm.
Keywords: Protocols, Petri nets, Verification, Model checking, Tool.
-
AWPN'95 (2. Workshop Algorithmen und Werkzeuge für Petrinetze - Oldenburg 95):
- Author: Bernd Grahlmann, Matthias Möller and Ulrich Anhalt
Abstract:
This paper introduces a special kind of parallel finite automata
(PFA) with B(PN)^2 actions as edge annotations. An algorithm for
the automatic translation into a B(PN)^2 program is described.
The algorithm is non-trivial because the structure of a PFA is
preserved in the generated B(PN)^2 program.
The modelling of the `Alternating-Bit' protocol using the parallel
composition of four finite automata (FA) is considered as an example.
The resulting B(PN)^2 program can be used directly as an input for
the current version of the PEP tool. Thus one further input
interface is provided to the user of the tool.
Keywords: Alternating-Bit-Protocol, B(PN)^2, Finite Automata, PEP.
-
ATPN'95 (Application and Theory of Petri Nets - Torino 95):
- Author: Bernd Grahlmann
Abstract:
The PEP system is not just another Petri net tool. Of
course it fullfills the main tasks of a good net tool.
It includes a high-level and a low-level net editor
with comfortable editing and simulating facilities.
In addition it offers a sophisticated verification
component based on a model checking algorithm using
partial orders. Thus various properties - given as
temporal logic formulae can be checked
efficiently.
But the PEP system is even more, it is a Programming
Environment based on Petri Nets. In PEP two of today's
most accepted theoretical approaches for the description
of parallel systems, Petri nets and process algebras, are
combined to model, simulate, analyse and verify parallel
systems. The application of both approaches using a
common, flexible parallel programming language called
B(PN)^2 (Basic Petri Net Programming Notation) is one of
the main characteristics of PEP.
Its comprehensive verification component allows to verify
a large range of properties of the parallel systems modelled
by the PEP tool. PEP has been implemented on Solaris 2.4,
SunOS 4.1.3 and Linux. An ftp-able version will be made
available shortly.
Keywords: Petri nets, Parallel Programming Language,
Simulation, Verification, Model checking, Tool.
-
Author: Bernd Grahlmann
Abstract:
PEP is a Programming Environment based on Petri Nets.
In PEP two of today's most accepted theoretical approaches for the
description of parallel systems, Petri nets and process algebras, are
combined to model, to simulate, to analyse and to verify parallel systems.
The application of both approaches using a common, flexible parallel
programming language called B(PN)^2 (Basic Petri Net
Programming Notation) is one of the main characteristics of PEP.
Its comprehensive verification component offers the possibility to
verify a large range of properties of the parallel systems modelled
by the PEP tool.
In this talk the fundamental objects -- B(PN)^2 programs, PBC (Petri
Box Calculus) expressions and Petri boxes -- will be
introduced. Considering the typical cycle of the usage of the
PEP system the interplay of these objects will be explained as will be
the basic functionality of the prototype.
This leads directly to the structure of the PEP system, i. e., the
composition and the interaction of the individual components constituting
the tool.
Finally the advantages of integrating the functionality in a graphical
user surface are emphasized by demonstrating the use of the tool
on an example.
-
Author: Bernd Grahlmann
Abstract:
The Programming Environment based on Petri Nets
PEP focuses its interest mainly on four kinds of objects well suited to model,
to simulate, to analyse and to verify parallel systems:
- Programs written in a dedicated parallel programming language
B(PN)^2 (Basic Petri Net Programming Notation)
- Programs expressed in a process algebra called PBC
(Petri Box Calculus)
- Petri boxes, which are a class of 1-safe labelled Petri nets
- Formulae given in a temporal logic.
A project management component is the central part of PEP.
Apart from editors for the kinds of objects just described, compilers
and analysis algorithms can be invoked.
This talk introduces the conception and the functionality of PEP.
It is augmented by examples of parallel systems being modelled
and verified by the tool. Performance results as well as other statistics
are presented. Finally an overview concerning future work is given.
Bernd Grahlmann Grahlmann@informatik.uni-oldenburg.de,
24.11.1998