?

• 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.
?