LMU München

Ludwig-Maximilians-Universität München
Programmierung und Softwaretechnik 

Univ.-Prof. Dr. M. Wirsing, Ordinarius
Univ.-Prof. Dr. F. Kröger, Extra-Ordinarius

Arbeitsschwerpunkte

• Software-Entwicklung unter Einbeziehung formaler Methoden
• Algebraische Spezifikationstechniken
• Softwaretechniken für multimediale Anwendungen
• Funktionale und objekt-orientierte Programmierung
• Semantik von Spezifikations- und Programmiersprachen
• Wiederverwendung von Software-Komponenten, Software-Bibliotheken
• Temporale Logiken und ihre Anwendungen
• Theorie paralleler Programme
• Constraint-Programmierung

Die Arbeitsgruppe PST setzt sich zur Zeit aus 17 Wissenschaftlern zusammen, die im Rahmen ihrer Forschung und Lehre Fragestellungen aus den Gebieten der Softwaretechnik und Programmierung bearbeiten. Dies umfaßt die formalen Grundlagen der Software-Entwicklung, objektorientierte und strukturierte Methoden des Software-Engineering, die Entwicklung und den Einsatz von CASE-Systemen, die Erprobung von Theorembeweisern, den Einsatz neuer Programmiersprachen (wie Java und Sicstus) und ihrer Erweiterungen (wie Pizza und CHR) zur Entwicklung von Anwendungen u.a. auf dem Gebiet der Internet- und Multimediaprogrammierung sowie in Entscheidungsunterstützungssystemen.

Ein vorrangiges Ziel der Lehr- und Forschungseinheit ist die Entwicklung von Methoden zur Verbesserung der Software-Qualität. Als Schlüssel dazu dient die Integration semiformaler Software-Engineering-Methoden, wie etwa OOSE, OMT und UML, mit formalen Methoden, da nur mit solchen auf mathematisch präzisen Notationen basierenden Beschreibungen von Anforderungen und Entwürfen Programme als fehlerfrei nachgewiesen werden können. Die Forschergruppe konzentriert sich dabei zum einen auf den Einsatz und die Weiterentwicklung algebraischer Spezifikationen, deren Grundlagen Ende der siebziger Jahre von Prof. Wirsing mitentwickelt wurden und die eine abstrakte Beschreibung von Softwarekomponenten erlauben.

Zum anderen wird die Verwendung Temporaler Logiken untersucht, die von Prof. Kröger mitentwickelt wurden und die einen formalen Zugang zur Beschreibung des Verhaltens paralleler Programme bieten. Zur Beschreibung verteilter nebenläufiger Systeme werden algebraische und temporale Spezifikationsansätze mit Termersetzungstechniken kombiniert und geeignet in eine objektorientierte Vorgehensweise eingebettet.

Ein zweites zentrales Thema ist die Entwicklung neuer abstrakter und/oder modularer Programmiertechniken. Für objektorientierte, constraint-basierte und funktionale Programmierung (in Sprachen wie Java, Eclipse, Sicstus, CHR und SML) werden sowohl grundlegende Aspekte wie Semantik, Korrektheit, Spezifikationskalküle untersucht als auch ihr Einsatz in praktischen Anwendungen, wie etwa in der Internetprogrammierung, bei Multimediasystemen und in Entscheidungsunterstützungssystemen, erprobt.

Gerade die Constraint-Programmierung führt schneller zu robuster, flexibler und wartbarer Software in Entscheidungsunterstützungssystemen, weil dieser Ansatz die deklarative Modellierung von Problemen und den korrekten Umgang mit ungenauen, unsicheren und unscharfen Daten erlaubt bei guter Kombinierbarkeit von Constraintlosen mit Such- und Optimierungsverfahren. Unser Lehrstuhl ist der Initiator der Arbeitsgruppe Constraints des Instituts für Informatik. Diese Arbeitsgruppe bietet: Zusammenarbeit mit Unternehmen und Behörden zum Einsatz der Constraint-Programmierung, Beratung zur Entwicklung von Entscheidungsunterstützungssystemen, Forschungsprototypen zu Weiterentwicklung und Vermarktung, und Unterstützung für Schulungen und Weiterbildung in Constraint-Programmierung.

Ein weiterer Forschungsschwerpunkt ist die Untersuchung und Erforschung von geeigneten Programmentwicklungstechniken, die die modulare Konstruktion von Software unter Einbeziehung der Wiederverwendung schon vorhandener Softwarekomponenten unterstützen. Durch die Wiederverwendung verifizierter (oder zumindest wohlerprobter) Softwarekomponenten soll neben der Verbesserung der Zuverlässigkeit von Softwaresystemen auch eine Reduzierung der Entwicklungskosten erreicht werden.

Projekte

(siehe auch Produkte und Werkzeuge)

In den letzten drei Jahren wurden u.a. folgende Forschungsprojekte erfolgreich abgeschlossen:

• Vigoni-Projekt ``Frameworks for Programming Logics'' Generelles Ziel dieses Projekts war die Erstellung formaler Methoden zur Entwicklung und Verifikation von Software.
• Projekt ``Mathematische Fundierung von Methoden des Software Engineering'' In diesem Projekt wurden pragmatische strukturierte Methoden aus der industriellen Praxis mit formalen, mathematisch fundierten Methoden der Softwareentwicklung integriert.
• EG-Projekte ``COMPASS'' und ``MeDiCis'' Im Rahmen dieser Projekte wurde gemeinsam mit europäischen Partnern ein umfassender algebraischer Ansatz zur Spezifikation und Entwicklung von Softwaresystemen untersucht.
• DAAD/PROCOPE-Projekt ``Kompositionale
  Spezifikation und Verifikation paralleler objektorientierter Systeme'' Das Projekt diente der Implementierung eines Model-Checking-Verfahrens für Agenten mit endlichem Zustandsraum.

   

Im folgenden werden die zur Zeit an der Lehr- und Forschungseinheit durchgeführten Forschungsprojekte genauer beschrieben:

EG/HCM-Projekt ``DeStijl: Entwurf und Spezifikation durch Sprachschnittstellen und -vereinigungen''

In diesem Projekt geht es um allgemeingültige Spezifikation- und Entwurfsprachen. Diese Sprachen sind der Kern rigoroser auf formalen Methoden basierter Softwareentwicklung. Die Erfahrung mit formalen Entwurf und Spezifikationsprachen tragen zu den aus der Situation in Programmiersprachen gelernten Lektionen bei: Die Notwendigkeit, existierende formale (exekutierbare oder nicht) Sprachen abzuändern, zu verbinden und zu erweitern, wird weiterbestehen. Dies verlangt eine ``Theorie des Sprachenengineering'', die als wissenschaftliche Basis für eine systematische Methodologie formaler Sprachenentwurf dienen kann.

DFG-Projekt ``Osidris: Objekt-orientierte Spezifikation und Verifikation von verteilten Systemen''

In diesem Projekt werden Methoden untersucht und erstellt, mit denen man paralleles Verhalten mit Objektorientierung auf abstrakter Ebene beschreiben, analysieren und verfeinern kann. Von besonderem Interesse ist dabei die Beobachtbarkeit und Vererbbarkeit von Eigenschaften der Datentypen und Objekte auf jeglicher Abstraktionsebene. Ziel dieses Projekts ist, das Zusammenspiel von objekt-orientierten Strukturierungsmechanismen und Parallelität zu verstehen und sinnvoll mit Spezifikations-, Verfeinerungs- und Beweismethoden zu kombinieren. Im ersten Projektabschnitt wurden Aspekte dieses Zusammenspiels untersucht. Dabei zeigte sich, das eine abstrakte Sprache (wie Maude) die Integration von objekt-orientierten und verteilten Mechanismen in sehr viel höherem Maße unterstützt als konventionellere Sprachen. Im zweiten Projektabschnitt sollen vor allem die Methoden der beobachtungsorientierten Verfeinerung und der Programmverifikation erweitert werden. Die dabei erlangten Erkenntnisse sollen zu einer Weiterentwicklung von Maude führen oder Alternativen auf der abstrakten Sprachebene anregen.

DAAD/ARC-Projekt ``ATMTS: Algebraische Werkzeuge zur Modellierung von Telekommunikationssystemen''

In diesem Projekt werden neue algebraische Modelle für industriell verwendete formale Beschreibungsmethoden erstellt. Im besonderen ist es unser Ziel, ein neues und vereinfachtes algebraisches Modell der vom IUT-T zum Standard erhobenen, industriell anerkannten Spezifikations- und Beschreibungssprache SDL zu schaffen, als eine strikte Basis zur Entwicklung neuer Algorithmen und Software-Werkzeuge für die Überprüfung der Standardeinhaltung, das Testen und die Verifikation. Wir wollen unser Modell und unsere Werkzeuge in mehreren von industriellen Projektpartnern initiierten Fallstudien erproben, unter anderem in Protokollen zur Implementierung der BISDN-Dienste unter Benutzung von ATM, sowie im Arbeitsverbund-BISDN-Dienst; dabei sollen Termersetzungstechniken zum Einsatz kommen.

Bayer. Forschungsstiftung - Projekt ``FORSOFT: Software-Engineering für verteilte Systeme in offenen Netzen''

Der Forschungsverbund FORSOFT ist eine Kooperation zwischen der Technischen Universität München, der Friedrich-Alexander-Universität Erlangen-Nürnberg, der Ludwig-Maximilians-Universität München, dem Forschungsinstitut für Angewandte Software-Technologie (FAST e.V.) sowie führenden bayerischen Firmen auf dem Gebiet des Software-Engineering. In fünf Projektbereichen arbeiten in 15 interdisziplinär angelegten Teilprojekten über 40 Mitarbeiter aus Hochschule und Industrie eng zusammen. Übergeordnete Zielsetzung ist die wissenschaftliche Fundierung, Systematisierung, Vereinheitlichung, Weiterentwicklung und Erprobung einer allgemeinen nutzer- und anwendungsorientierten Methodik, sowie von Beschreibungstechniken, Projektorganisation und -management im Software-Engineering. Dies beinhaltet Grundlagenfragen bei der Organisation des Entwicklungsprozesses ebenso wie die Entwicklung heterogener Systeme im Hardware-/Software-Codesign mit Echtzeitanwendungen.

Industrie-Projekt ``CafeOBJ''

Ziel des CafeOBJ-Projektes ist es, formale Methoden Softwareingenieuren in der Praxis zugänglich zu machen. Formale Methoden beinhalten die Aufstellung mathematischer Modelle und die Ableitung einiger Softwareeigenschaften aus diesen Modellen. Dieses Vorgehen hat Parallelen in anderen Ingenieursbereichen, stellt aber wegen der enormen Komplexität moderner Softwaresysteme und der Unerfahrenheit der Entwickler mit höherer diskreter Mathematik für das Gebiet der Softwareentwicklung erhöhte Anforderungen. Die CafeOBJ-Sprache erweitert das ursprüngliche OBJ um Konzepte verteilter objektorientierter Systeme. Die Münchener Gruppe befaßt sich hauptsächlich mit Fallstudien. Diese umfassen: 

• die Implementierung von Fallstudien des fOOSE-Projekts in CafeOBJ,
• die Entwicklung und Testung von CafeOBJ-Spezifikationen für den Flughafen München II,
• die Formalisierung einer Semantik der objektorientierten, parallelen Programmiersprache Java in CafeOBJ.

DFG-Projekt ``Constraints: Funktional-Logische Programmierung mit Constraints''

Ziel dieses gemeinsam mit der Universität Karlsruhe durchgeführten Projekts ist die semantisch wohlfundierte Integration von funktionalen und constraint-basierten Programmierkonzepten in Form einer schlanken, auf den Lambda-Kalkül gestützten Kernsprache. Für diese Kernsprache sollen eine denotationale als auch eine operationale Semantik angegeben und deren Eigenschaften gezeigt werden, wie die Church-Rosser-Eigenschaft, die Adäquatheit der operationalen bezüglich der denotationalen Semantik und die oberservationale Erweiterung des Lambda-Kalküls. Anwendbarkeit und Ausdruckstärke der Kernsprache werden mit Hilfe von Fallstudien untersucht. Die Fallstudien beinhalten die Modellierung imperativ-funktionaler Programmierung und logischer Programmierung sowie Beispiele aus der Produktions- und Zeitplanung. Zur Durchführung der Fallstudien ist die Implementierung eines Prototypinterpreters geplant.

Projekt ``CHR: Die Constraint Handling Rules Sprache''

Komplexe Probleme lassen sich mit der Constraint-Programmierung direkt formulieren und effizient lösen. Erfolgreiche kommerzielle Anwendungen existieren in der Produktions- und Ressourcenplanung, Personalplanung, Transportoptimierung, Layoutgenerierung und in CAD-Systemen ebenso wie in der Finanzanalyse. Constraint Handling Rules (CHR) ist eine spezielle Programmbibliothek zur Spezifikation und Implementierung von Constraintlosern in höheren Programmiersprachen. In CHR drucken nebenläufige, logische Regeln aus, wie sich Constraints vereinfachen und wie sie neue Constraints propagieren. Die CHR-Sprache ermöglicht die schnelle Erstellung von Prototypen, von Erweiterungen, von Spezialisierungen und von Kombinationen von Constraintlösern. CHR sind eine Spracherweiterung, die in eine Programmiersprache als Bibliothek eingebettet werden können. In der Basissprache werden Programme geschrieben, die dann die in CHR implementierten Constraints benutzen können. Andrerseits können CHR-Programme in der Basissprache implementierte Prozeduren als Hilfsprozeduren verwenden. CHR sind weltweit in mehr als zwanzig Projekten im Einsatz.

Veröffentlichungen

(nur ab 1996)

• Alexander Knapp and Nora Koch. Epkml: A Specification Language for Electronic Product Catalogues. IEEE Multimedia, to appear, 1998.
• Pietro Cenciarelli, Alexander Knapp, Bernhard Reus, and Martin Wirsing. From Sequential to Multi-Threaded Java: An Event-Based Operational Semantics. In Proc. 6th Int. Conf. Algebraic Methodology and Software Technology, LNCS, Berlin, 1997. Springer.
• T. Frühwirth and S. Abdennadher. Constraint-Programmierung, Lehrbuch, Springer Verlag, 1997.
• Martin Abadi, Leslie Lamport, and Stephan Merz. A TLA solution to the RPC-Memory specification problem. In Manfred Broy, Stephan Merz, and Katharina Spies, editors, Formal System Specification: The RPC-Memory Specification Case Study, volume 1169 of LNCS, pages 21-66. Springer-Verlag, Berlin, 1996.
• Rolf Hennicker, Martin Wirsing, and Michel Bidoit. Proof systems for structured specifications with observability operators. Theoretical Computer Science, 1996.
• Piotr Kosiuczenko and Karl Meinke. On the Power of Higher-Order Algebraic Specification. Information and Computation, number 124, pages 85-101, 1996.

   

Produkte und Werkzeuge

In den letzten drei Jahren wurden u.a. folgende Produkte und Werkzeuge entwickelt:

Projekt ``Reisekostensystem der Universität München''

In diesem Projekt wurde ein System zur Abrechnung von Reisen nach dem Bayerischen Reisekostengesetz in Kooperation mit dem Bayerischen Finanzministerium, der Bezirksfinanzdirektion Regensburg und dem Referat IIIA5 der Universität München entwickelt.

Projekt ``CSDM: Entwicklungsunterstützung für den Entwurf korrekter Software''

CSDM ist ein Software-Entwicklungs-System, das den Entwurf korrekter Software durch die Einbeziehung formaler Methoden und die Wiederverwendung bereits erstellter Softwarekomponenten unterstützt.

BMBF-Projekt ``EPKfix: Methoden und Werkzeuge zur effizienten Erstellung elektronischer Produktkataloge''

Das Verbundforschungsprojekt entwickelte Verfahren und Werkzeuge zur Unterstützung des gesamten Lebenzyklus von elektronischen Produktkatalogen (EPKs). Ausgehend von einer umfassenden Analyse praxisrelevanter elektronischer Kataloge stand dabei die Entwicklung einer Spezifikationssprache für EPKs ebenso im Mittelpunkt wie geeignete Werkzeuge zur Unterstützung der Anforderunganalyse, der Formalisierung von EPKs, der Realisierung weitreichender Services für EPKs und umfassender automatischer Tests.

Im folgenden werden die zur Zeit an der Lehr- und Forschungseinheit durchgeführten Produkt- und Werkzeugentwicklungen genauer beschrieben (siehe auch Projekte):

Industrie-Projekt ``Simulation und Analyse von Statecharts''

In Zusammenarbeit mit der BMW AG verwenden wir Constraint-Programmierung mit CHR, um Software, die durch Statecharts beschrieben ist, abstrakt ablaufen zu lassen. Dies bedeutet, daß die Problemparameter und Programmvariablen keine konkreten Anfangswerte erhalten, sondern im Lauf der Abarbeitung durch Constraints immer mehr eingeschränkt werden, so daß am Ende eine abstrakte Beschreibung der Voraussetzungen zu Verfügung steht, die zu einem bestimmten, gewünschten Endergebnis führen. Damit lassen sich auch Testfälle generieren.

Projekt ``IMS: Der Münchner Mietspiegel im Internet''

Der elektronische Mietspiegel im World-Wide-Web (IMS) erlaubt es, in wenigen Minuten die ortsübliche Vergleichsmiete einer Wohnung zu berechnen. Einige Fragen des Münchner Mietspiegels sind schwer zu beantworten. Man benötigt Angaben, über die man in der Regel nur ungenügend Bescheid weiß, z.B. das genaue Baujahr des Hauses oder die Höhe der Kachelung im Bad. Mittels Constraint-Technologie ist der elektronische Mietspiegel sogar in der Lage, mit ungenauen und unvollständigen Angaben umzugehen. Damit läßt sich erstmals ein Mietspiegel auch dazu verwenden, bei der Wohnungssuche das Mietpreisniveau zu bestimmen, ohne sich auf eine bestimmte Wohnung festlegen zu müssen. Dieser preisgekrönte Service wurde. 1996 fast 10.000 mal benutzt. Projektpartner sind der Lehrstuhl für Programmierung und Modellierungssprachen, Prof. Broy, LMU München und die ECRC GmbH in München.

Kontaktadresse:

Univ.-Prof. Dr. M. Wirsing, Ordinarius
Univ.-Prof. Dr. F. Kröger, Extra-Ordinarius
Ludwig-Maximilians-Universität München
Programmierung und Softwaretechnik
Oettingenstr. 67, 80538 München
Tel.: (089) 2178-2151, Fax: 2152