Overview

Petri-Netze und damit verwandte Systemmodelle sind zur Spezifikation, formalen Untersuchung und zur Simulation von Software in verschiedenen Phasen der Entwicklung komplexer Rechensysteme geeignet. In diesem Bericht werden 22 existierende Software-Werkzeuge (ohne Anspruch auf Vollständigkeit) klassifiziert und bewertet, die jeweils eine Teilmenge der denkbaren Untersuchungsmethoden unterstützen, bzw. einen graphischen Editor zur Netzkonstruktion aufweisen. Klassifikation und Bewertung der Merkmale erfolgten mittels eines speziellen Beschreibungskatalogs. Dabei wird erstmals versucht, die wichtigsten Klassen von Petri-Netzen zu bestimmen. Der zweite Teil des Berichts beschreibt informell (an Hand eines Beispiels) und formal (Definition der verwendeten Netzklassen und aller darauf realisierten Analyseverfahren) das Petri-Netz-Werkzeug PROVER (PRedicate/Transition Net Oriented VERification System). Neben einer Bestandsaufnahme von Petri-Netz-Werkzeugen werden im Buch formale Spezifikationsverfahren mit höheren Petri-Netzen in der Anwendung gezeigt, um einen formalen Zugang zu ermöglichen.

Full Product Details

Author:   Marek Leszak ,  Horst Eggert
Publisher:   Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
Imprint:   Springer-Verlag Berlin and Heidelberg GmbH & Co. K
Volume:   197
Dimensions:   Width: 17.00cm , Height: 1.40cm , Length: 24.40cm
Weight:   0.475kg
ISBN:  

9783540506423

ISBN 10:   354050642
Pages:   254
Publication Date:   14 December 1988
Audience:   Professional and scholarly ,  Professional & Vocational
Format:   Paperback
Publisher's Status:   Active
Availability:   Out of stock  
The supplier is temporarily out of stock of this item. It will be ordered for you on backorder and shipped when it becomes available.
Language:   German

Table of Contents

1 Einleitung.- 2 Eine Klassifikation Von Petri-Netz-Klassen.- 2.1 Grobklassifikation.- 2.2 Feinklassifikation.- 2.2.1 Stellen-Parameter.- 2.2.2 Transitions-Parameter.- 2.2.3 Kanten-Parameter.- 2.2.4 Markenidentifikations- und Markenstruktur-Parameter.- 2.2.5 Stochastische Parameter.- 2.3 Zusammenfassung.- 2.4 Klassifikation gangiger Netzklassen.- 3 Eine Klassifikation Von Spezifikation- und AnalysemethoDen Fur Petri-Netze.- 3.1 Spezifikations-Schnittstelle.- 3.1.1 Netzeditor.- 3.1.2 Konstruktions-Unterstutzung fur grosse Netze.- 3.1.3 Operationen auf Subnetzen.- 3.1.4 Speicherung von und Zugriff auf Netze.- 3.2 Invarianten-Analyse.- 3.3 Erreichbarkeits-Analyse.- 3.3.1 Konstruktion des Erreichbarkeits-Graphen.- 3.3.2 Dynamische funktionelle Validation durch Erreichbarkeits- Analyse.- 3.3.3 Quantitative Validation auf Erreichbarkeits-Graphen durch Markovketten-Analyse.- 3.4 Diskrete Simulation.- 3.5 Programm-und Netz-Generation.- 3.6 Netz-Reduktion.- 4 Klassifikation und Bewertung Existierender Petri-Netz-Werkzeuge.- 4.1 Beschreibungs-Katalog fur Petri-Netz-Werkzeuge.- 4.2 Klassifikation und Bewertung existierender Werkzeuge auf hoeheren Petri-Netzen.- 4.3 Zusammenfassung.- 5 Auswahl Geeigneter Petri-Netz-Werkzeuge.- 5.1 Werkzeuge zur graphischen Netzkonstruktion.- 5.2 Werkzeuge zur strukturellen funktionellen Validation durch Invarianten-Analyse.- 5.3 Werkzeuge zur dynamischen funktionellen Validation durch Erreichbarkeits-Analyse.- 5.4 Werkzeuge zur quantitativen Validation durch Markovketten-Analyse.- 5.5 Werkzeuge zur quantitativen Validation durch Simulation.- 5.6 Werkzeuge zur Programm-Generation und zur Netzreduktion.- 5.7 Zusammenfassung.- 6 Funktionalitat und Benutzeroberflache Des Petri-Netz-Werkzeuges 'Prover'.- 6.1 UEberblick uber das Petri-Netz-Werkzeug 'PROVER'.- 6.2 Modellbeschreibung eines Multi-tasking Monitors.- 6.2.1 Informelle Beschreibung.- 6.2.2 PDL-Spezifikation.- 6.3 Ergebnisse der Erreichbarkeitsanalyse.- 6.3.1 Stellen-und Variablen-Information.- 6.3.2 Dynamisches Verhalten von Transitionen.- 6.3.3 Starke Zusammenhangs-Komponenten.- 6.3.4 Anfragen zur Selektion von Markierungs-Teilmengen.- 6.3.5 Fehler-Erkennung: Kapazitats-UEberlauf.- 6.3.6 Fehler-Erkennung: tote Stellen und Transitionen.- 6.3.7 Fehler-Erkennung: Deadlocks bzw. Endzustande.- 6.3.8 Fehler-Erkennung: Livelocks.- 6.3.9 Reproduzierbare Markierungen.- 6.3.10 Homezustande.- 6.3.11 Gemeinsame Folgezustande.- 6.3.12 Konflikte zwischen Transitionen.- 6.4 Ergebnisse der S-Invarianten-Analyse.- 7 Ausblick.- 7.1 Fortgeschrittene Spezifikationssprachen fur hoehere Netze.- 7.1.1 Erweiterung der PDL um hoehere funktionale Konstrukte.- 7.1.2 Hierarchische Netzspezifikation.- 7.2 Fortgeschrittene Analysemethoden auf hoeheren Netzen.- 7.2.1 Neue Konstruktionsverfahren fur Erreichbarkeitsgraphen.- 7.2.2 Analyse von Synchronie- und Fairness-Eigenschaften.- 7.2.3 Analyse toter dynamischer Netzteile (gefrorene Marken).- 7.2.4 Programm-und Netz-Generierung.- 7.3 Fortgeschrittene integrierte Petri-Netz-Werkzeuge.- 8 Anhang A: Prover-Online-Dokumentation.- 8.1 PROVER-Kommandos.- 8.2 PDL-Compiler 'PDLC'.- 8.3 Erreichbarkeitsgraph-Generator 'RGG'.- 8.4 Erreichbarkeitsgraph-Anfragesystem 'RGI'.- 9 Anhang B: Syntax und Semantik der Spezifikationssprache 'PDL' (Predicate/Transition Net Description Language).- 9.1 In PROVER realisierte PDL.- 9.2 Entwurf einer erweiterten PDL.- 10 Anhang C: Definition Und Eigenschaften Der Pradikat/Tr Ansitions-Netze.- 10.1 Pradikatenlogische und mengentheoretische Grundlagen.- 10.2 Pradikat/Transitions-Netz.- 10.3 Erreichbarkeits-Graph.- 10.4 Konflikte und Kontakte.- 10.5 Starke Zusammenhangs-Komponenten.- 10.6 Lebendigkeits-Eigenschaften.- 10.7 Fairness-Eigenschaften.- 10.8 Gefrorene Marken.- 10.9 Abbildungen der Beispiele.- Anhang D Glossar.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions