26th IFIP WG 6.1 International Conference on
Formal Methods for Networked and Distributed Systems
Special focus on verified middleware and distributed services
From Formal Specification to Software Design
A tutorial on modelling, design and verification of software systems using Petri nets
by Prof. Rüdiger Valk, Univ. Hamburg, Germany
Nowadays, computer-based systems are indispensable for almost all areas of modern life. As has been frequently stated, they suffer, however, from being insufficiently correct or reliable. Software development projects fail their completion deadlines and financial frames. Though computer systems surpass in size all traditional complex systems ever produced, the discrepancy in quality standards seems to be unbridgeable.As shown by concrete projects, there are many reasons that Petri nets contribute to overcome these problems:
- Petri nets exhibit a graphical, a textual and a formal representation. This is mirrored by the fact that powerful graphic-tools have been developed, that they can be used like a programming language and that there is a large pool of effective algorithms.
- Petri nets support model-based development approaches, leading to similar representations of abstract system models and concrete implementations.
- Petri nets are used as round-trip engineering method, strongly supporting the transition from modelling, to analysis and implementation with minimal loss of information.
- Petri nets are suitable for the modelling and implementation of synchronous systems as well of distributed systems which are ubiquitous in current applications.
- Methods of refinement and abstraction allow to use Petri nets like low level languages as well as component-based abstract concepts, that are linked by strong methods.
- Petri nets are field-tested in applications in the context of technical and embedded systems, using methods of traditional engineering
- More recently, Petri nets support systems incorporating human and machine/human interactions by using methods related to workflow-systems, object- and agent-oriented approaches. In particular object Petri nets have been successfully used to model mobile agents with respect to very different aspects, including sociological and psychological approaches.