Martin Wirsing, Harald Störrle (Ludwig-Maximilians-Universität München):
Debugging ROOM Designs using High-Level-Petri-Nets
The functional evolution (read: maintenance) of large software systems
has been a largely unanswered challenge ever since. Obviously, working
on the code level has not solved the problem. Working on the design
level might be a step ahead.
In this lecture we present an approach for validating design
specifications written in the Unified Modelling Language (UML) and
the component-model of the ROOM method. Semantically, design diagrams
are represented by structured high-level Petri-nets. An abstract
syntax for ROOM components, sequence diagrams, and state charts is
introduced and a translation from syntax to semantics is provided.
Then we show how the well-known validation and consistency criteria
of Petri-nets can be applied to design specifications.
This way, it is possible to validate designs by interactive
simulation of the semantical object corresponding to a design diagram,
to automatically ensure and check consistency conditions, and to
prove many interesting properties such as safety and lifeness.
Colloquium home page
