direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Habilitationen 2006

Habilitationsvortrag

Formale Spezifikation und regelbasierte Verfeinerung von Software-Komponenten Formale Spezifikation und regelbasierte Verfeinerung von Software-Komponenten - Eine formale Komponententechnik
Frau Dr.-Ing. Julia Padberg, Berlin
Mittwoch, 15. Februar 2006 um 12.00 Uhr, Raum FR 5516

Software-Entwicklung braucht zunehmend formale Konzepte und Modellierungstechniken, da die rasant steigende Komplexität der zu entwickelnden Systeme häufig die Konsistenz dieser beeinträchtigt. Die formalen Techniken sind selbst wieder von unterschiedlichem Abstraktionsgrad, solche die direkt die Software-Entwicklung unterstützen bis hin zu solchen, die abstrakte Konzepte, die auf den formalen Techniken basieren, formalisieren. Die formale Komponententechnik, wie sie in diesem Vortrag vorgestellt wird, ist auf einem solchen hohen Abstraktionsgrad formuliert. Software-Komponenten stellen einen allgemein anerkannten Strukturierungsmechanismus dar, der während des gesamten Lebenszyklus eines Software-Systems von der Analyse bis zur Wartung eingesetzt wird. Komponentenbasierte Software-Entwicklung benötigt formale Komponentenkonzepte, um die nichtdeterminierte und nebenläufige Interaktion der Komponenten präzise zu beschreiben und damit ein Haupthindernis für die Anpassung an sich ändernde Systemumgebungen zu überwinden.

Die vorgestellte formale Komponententechnik, die eine formale Komponentenbeschreibung, ihre Semantik, Kompositionsoperationen sowie die Verfeinerungskonzepte umfasst, ist für die formale Fundierung der komponentenbasierten Entwicklung geeignet. Die formale Beschreibung der Komponentenschnittstellen sowie der Komponentenspezifikation erlaubt die gründliche mathematische Modellierung und die Verifikation der gewünschten Funktionalität. Die Konzepte dieser Komponententechnik werden in einem Beispiel, das auf Petrinetzen basiert, veranschaulicht und die Resultate anhand dieses Beispiels diskutiert.

Wir diskutieren unterschiedliche Instantiierungen, wie algebraische Spezifikationen, Automaten, Petrinetze und Graphtransformationssysteme. Petrinetztransformationen und Petrinetzmodule werden tiefer gehend untersucht, um darzustellen, dass diese Konzepte, die aus der Datentypspezifikation stammen, auch für Prozessspezifikationen geeignet sind. Nichtsdestotrotz sind die Begriffe und Ergebnisse auch in den anderen Instantiierungen verfügbar.

Zusatzinformationen / Extras

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe

Diese Seite verwendet Matomo für anonymisierte Webanalysen. Mehr Informationen und Opt-Out-Möglichkeiten unter Datenschutz.