• Algebraische Kalküle für Separationslogik (AlgSep), 2011

Das Projektziel ist, aufbauend auf einem bereits vorhandenen Grundstock, eine algebraische Darstellung separationslogischer Kalküle. Hierbei liegt das Hauptaugenmerk auf der algebraischen Charakterisierung und deren Verwendung für Verifikationsaufgaben. Als positiver Nebeneffekt soll genützt werden, dass durch Algebraisierung Verifikationsaufgaben mittels bereits vorhandener Beweissysteme durchgeführt werden können.

 

• Algebra-Basierte Feature-Orientierte Programmsynthese (FeatureFoundation), 2009

Das Projekt FeatureFoundation hat zum Ziel, bisherige Arbeiten unter dem Ansatz der Algebra-Basierten Feature-Orientierten Programmsynthese zu vereinheitlichen. Die Synthese von Programmen aus Features soll weitestgehend automatisiert und auf ein solides formales Fundament gestellt werden.
 

 

• DFG-Forscherverbund InopSys - Interoperabilität von Kalkülen für die Systemmodellierung, 2006

Ausgangspunkt ist dabei, dass nach Auffassung nahezu aller neueren praktischen System­be­schrei­bungssprachen komplexe informationsverarbeitende Systeme am verständlichsten in unter­schiedlichen, komplementären Sichten beschrieben werden. Dazu dient eine Reihe grundlegend verschiedener Modelle für die relevanten Aspekte wie Daten, Zustands­über­gänge, Interaktion, Komposition, rekursive Definitionen auf allen Ebenen, sowie Dynamik und Mobilität in sich konfigurierenden Netzen. Ziel ist eine Zusammenführung der unterschiedlichen formalen Modelle in ein interoperables Baukastensystem.

 

• Entwicklung von Graphenalgorithmen in formalen Kalkülen, 2002

Projektziel war ein praktikabler algebraischer Kalkül, der besonders zur Entwicklung generischer, also hochgradig wiederverwendbarer, Graphenalgorithmen aus ihren formalen Spezifikationen geeignet ist. Es zeigte sich, daß neben dem klassischen Relationenkalkül vor allem die Kleene-Algebra mit Vor- und Nachbereichsoperator hervorragend geeignet ist.
 

• Systemunterstützung für die Algebraische Systementwicklung , 2002

Das Projekt diente dazu, eine lose Zusammenarbeit mit dem Kestrel Institute, Palo Alto, zu etablieren. Es behandelt die folgenden Themen: Erstens wird die Augsburger Gruppe das Kestrel-System "SPECWARE" im Hinblick auf seine Eignung für die Unterstützung algebraischer Herleitungen evaluieren. Zweitens wird Kestrel untersuchen, wie die Augsburger Formalisierung von Zeigerstrukturen in einer konkreten Modellierungs- und Verifikationsaufgabe eingesetzt werden kann.
Drittens werden beide Gruppen auf dem Gebiet der formalen algebraischen Entwicklung nebenläufiger Speicherbereinigungsalgorithmen kooperieren.
Homepage

 

• Ausbau des Multimedia-Einsatzes in der Lehre an den Universitäten (JPP), 2000

Im Rahmen des Förderprogramms "Ausbau des Multimedia-Einsatzes in der Lehre an den Universitäten" des Bayerischen Staatsministeriums für Wissenschaft, Forschung und Kunst wurden Werkzeuge zur Erzeugung multimedialer Vorlesungen erstellt.

Homepage

 

• Entwurfsmethodik für reaktive Systeme , 1998

Ein Projektziel war die Erarbeitung von Techniken zur schrittweisen Entwicklung von reaktiven Systemen. Konkret sollte untersucht werden, ob sich Statecharts für die dazu erforderlichen Verfeinerungs- und Transformationsschritte eignen oder ob die Sprache angepaßt werden muß, um solche Schritte zu ermöglichen. Weiter wurden im Projekt Techniken zur Partitionierung von Statecharts für deren verteilte Implementierung entwickelt.
 

• New Hardware Design Methods (ESPRIT Working Group 8533 NADA), 1998

Das Projekt erforschte neue, mathematisch fundierte Methoden für Beschreibung und Entwurf von Hardwaresystemen. Dabei wurde der Begriff "Hardwaresystem" sehr allgemein aufgefaßt, so daß er gleichermaßen Architekturen, Schaltungen und Die Schnittstelle von Hardware und Software abdeckte. Ein weiteres Projektziel war ein Vorentwurf für eine Hardwarebeschreibungssprache der nächsten Generation, mit hohem Abstraktionsniveau und sauberer und vollständig formaler Semantik.
Unter die Beschreibungsaspekte fielen allgemeine Fragen von Zeitabhängigkeiten, Parametrisierung und Modularisierung. Die Entwurfstechniken umfaßten Verifikation, deduktiven Entwurf im Kleinen und strukturierten Entwurf im Großen. Mit den Untersuchungen zur Modellierung sollten Anforderungen an Entwurfsmethodiken und Beschreibungssprachen herausdestilliert werden. Das Projekt behandelte Architekturen, Schaltungen, neu entstehende Paradigmen für Hardwaresysteme sowie verschiedene Standardtechnologien; es führte zu vereinheitlichten mathematischen Hardwaremodellen. Geeignete mathematische Methoden stammten aus Berechenbarkeitstheorie, Algebra höherer Stufe, Beweistheorie und Prozessalgebra mit Zeit. Die entwickelten Techniken wurden anhand repräsentativer Fallstudien demonstriert.

 

• Deduktiver Entwurf paralleler Soft- und Hardwaresysteme , 1995

Ein Projektziel war eine einheitliche formale Entwurfsmethodik für paralleler Soft- und Hardwaresysteme. Als Fallstudie diente ein Schaltwerk für einen asynchronen beschränkten Schlangenpuffer, das als eine der IFIP WG 10.2 Verification Benchmarks diente. Die formale Analyse ergab, daß die dort angegebene Schaltung fehlerhaft war; der Fehler hätte durch systematische Anwendung der Technik des Deduktiven Entwurfs vermieden werden können. Weitere Untersuchungen betrafen die Verwendung von Kommunikationsströmen bei der Hardwarebeschreibung und -entwicklung.

 

• Spezifikation informatischer Systeme in Logik höherer Stufe, 1994

Bei der Methode der algebraischen Spezifikation werden Datenstrukturen durch ihre typischen Operationen und die zwischen ihnen herrschenden Gleichungsgesetze charakterisiert. Während dieser Ansatz zunächst auf Operationen erster Stufe beschränkt war, hatten die zentralen Projektpartner, K. Meinke und B. Möller, Pionierarbeit darin geleistet, ihn auf den Fall von Operationen höherer Stufe zu erweitern.
Das Projekt befaßte sich mit der Weiterentwicklung der zugrunde liegenden mathematischen Theorie sowie mit Fallstudien zum Einsatz dieser Methode. Speziell wurden Untersuchungen zur Klassifikation der Ausdrucksstärke und zur Berechenbarkeit von Modellen von Spezifikationen höherer Stufe angestellt.
 

• Transformationeller Entwurf paralleler Algorithmen, 1994

Ziel des Projekts war die übertragung der Technik der ransformationellen Programmentwicklung auf die Entwicklung paralleler Algorithmen für verschiedene Architekturklassen aus der problemnahen Spezifikation ihres Ein-/Ausgabeverhaltens.
Projektbeschreibung, Veröffentlichungen

 

• Formale Entwicklung digitaler Schaltungen, 1993

Projektziel war es, aus den allgemeinen Regeln der Programmkonstruktion solche abzuleiten, die im Spezialfall der Schaltungsentwicklung besonders adäquat und bequem zu handhaben sind.
 

• Funktionale Modellierung verteilter Systeme, 1992

Die Arbeiten zielten auf die Erstellung eines formalen, auf funktionale Beschreibungstechniken gegründeten Entwurfsrahmens, innerhalb dessen verteilte Systeme systematisch entwickelt werden können. Besondere Berücksichtigung fand dabei der Schaltwerksentwurf.