Zum Hauptinhalt springen

Universität Ulm

Universität Ulm 
Fakultät für Informatik 
Abt. Programmiermethodik und Compilerbau 

Prof. Dr. H. A. Partsch

 

Arbeitsschwerpunkte

  • Integration konventioneller und formaler Methoden des Software Engineering
  • Algebraisch basierte Spezifikation und Programmtransformation
  • Entwicklungsmethodik für datenparallele Programme
  • Requirements Engineering
  • Übersetzerbau
  • Eingebettete Systeme
  • Funktionale Programmierung

 

Projekte

Experimentelles Software Engineering für eingebettete Systeme

Verläßliche Aussagen über die Qualität von Methoden und Techniken des Software Engineering scheitern derzeit am Fehlen entsprechender quantitativer nachvollziehbarer Erfahrungen. Zielsetzung dieses Kooperationsprojekts mit der Daimler-Benz-Forschung im Rahmen des Softwarelabors Ulm ist es, durch Konzeption und Durchführung geeigneter Experimente mit Studentengruppen verläßliches Zahlenmaterial über Vorgehensweisen bei der Entwicklung von Echtzeit-Systemen zu gewinnen. Eine vergleichende Studie verschiedener SA/RT-Methoden und Werkzeugen ist bereits ebenso erfolgreich abgeschlossen, wie eine (ebenfalls) vergleichende Untersuchung über Kosten/Nutzen statischer und dynamischer Prüfverfahren sowie eine weitere Studie, in der strukturierte und objektorientierte Analysemethoden miteinander verglichen wurden. Eine Fortsetzung der letzten Studie, in der der Einfluß der gewählten Analysemethode auf Entwurf und Implementierung untersucht werden soll, findet derzeit statt.

Ebenfalls Inhalt der Arbeit des Softwarelabors sind Evaluationsstudien marktgängiger Softwarewerkzeuge im Rahmen von Individualpraktika und Diplomarbeiten.

Fortgeschrittene Werkzeuge für die funktionale Programmierung

Die Vorteile der deklarativen Programmierung (funktional, logisch, algebraisch-axiomatisch) sind im Prinzip weitgehend unbestritten. In der Praxis allerdings haben sich diese ,,neuen`` Paradigmen noch nicht etabliert, was vor allem darauf zurückzuführen ist, daß hinreichend mächtige Werkzeuge zu ihrer Unterstützung entweder fehlen oder die erwähnten Vorteile nicht entsprechend nutzen. In dem Projekt werden unterschiedliche Möglichkeiten der Werkzeugunterstützung für verschiedene deklarative Ansätze untersucht.

Ein Resultat dieser Aktivitäten ist TkGofer. Dabei handelt es sich um eine funktionale Bibliothek für graphische Benutzeroberflächen, die eine typsichere, abstrakte und strukturierte Oberflächenprogrammierung ermöglicht. Aufbauend auf TkGofer sind eine Reihe kleinerer Werkzeuge entstanden, hauptsächlich für die Animation oder Visualisierung von Problemen aus dem Bereich des Übersetzerbaus. Darüberhinaus wurde TkGofer erfolgreich bei der Integration eines SQL-Datenbanksystems in eine funktionale Sprache sowie bei der Implementierung eines automatischen Programmoptimierers eingesetzt.

Derzeit in Arbeit ist die Entwicklung von ULTRA, ein interaktives System, das die transformationelle Entwicklung funktionaler Programme unterstüzt.

Quellsprachen-Optimierung für Echtzeitcompiler

Echtzeitcompiler übersetzen gängige Programmiersprachen (wie C und C++) in speziell für die Steuerung eingebetteter Systeme mit Echtzeitbedingungen abgestimmten Code. Aufgrund der beschränkten Möglichkeiten der diesen Code ausführenden Prozessoren ergeben sich zusätzliche Anforderungen an diesen Code, einerseits im Hinblick auf die Effizienz, andererseits im Hinblick auf die Vorhersagbarkeit der Ausführungsdauer dieses Codes. In diesem Projekt, das in Kooperation mit einem industriellen Partner durchgeführt wird, sollen verschiedene Techniken der Quellsprachen-Optimierung auf ihren Nutzen hin analysiert und prototypisch implementiert werden.

FOX: Formale objekt-orientierte Softwareentwicklung

Die Notwendigkeit des Einsatzes formal fundierter Methoden in der Software-Entwicklung, insbesondere im Zusammenhang mit sicherheitskritischer Software, als Alternative zum (konventionellen) Software Engineering wird zunehmend erkannt und akzeptiert. Andererseits haben sich auch gewisse Erkenntnisse und Vorgehensweisen des (konventionellen) Software Engineering in der Praxis bewährt (z. B. objektorientierte Entwicklungsmethoden), so daß es wenig zweckmäßig und ökonomisch unsinnig wäre, darauf gänzlich zu verzichten. Zielsetzung dieses Projekts ist es, durch geeignete Symbiose und Integration die jeweiligen Vorteile beider Vorgehensweisen geschickt zu kombinieren, um so langfristig zu einem mathematisch fundierten Software Engineering zu kommen. Untersucht wurde u.a. die Kombination von modellbasierten Spezifikationsmethoden (wie Z) mit objektorientierten Ansätzen für die Analyse und den Entwurf von Softwaresystemen. Im Moment konzentriert sich die Arbeit auf die Erweiterung der Entwicklungsmethode um eine Requirements Engineering-Phase zur formalen Definition der Systemanforderungen.

Semantik, Übersetzerspezifikation und Bytecode-Verifikation für Java

Java ist eine von Sun entwickelte, klassenbasierte, objektorientierte Programmiersprache. Zielsetzung ihres Entwurfs war Portabilität und Sicherheit. Letztere wird durch strenge statische Typisierung, Abstraktion von dynamischer Speicherallokation, Laufzeitüberprüfungen sowie einen Sicherheitsmanager gewährleistet. Glaubwürdige Sicherheitsmodelle erfordern formale Spezifikationen, die für Java zur Zeit noch nicht vorliegen. Im laufenden Projekt werden daher formale Spezifikationen für Java, für ihre virtuelle Maschine sowie für ausgewählte Bibliotheksklassen angegeben. Ferner entsteht eine Übersetzerspezifikation, bei deren Einhaltung ein Java Compiler korrekten Code erzeugt. Da Javas virtuelle Maschine jedoch nicht nur Code von semantikbewahrenden Compilern verarbeiten sondern auch Code aus fremden Quellen sicher ausführen können muß, ist ein formal entwickelter Bytecode-Verifier ein weiterer notwendiger Baustein eines Sicherheitsmodells für Java.

Veröffentlichungen

  • K. Achatz, W.Schulte.  Massive Parallelization of Divide-and-Conquer Algorithms over Powerlists. Science of Computer Programming, 26, (1996) 59 - 78.
  • K. Achatz, W.Schulte.  Formale objektorientierte Softwareentwicklung mit Fox. Erscheint demnächst in der Zeitschrift Informatik, Forschung und Entwicklung. Springer-Verlag 1998.
  • E. Börger, W. Schulte. A Programmer Friendly Modular Definition of the Semantics of Java. In: J. Alves-Foss (ed.), Formal Syntax and Semantics of Java, LNCS, Springer-Verlag 1998.
  • B. Möller, H. Partsch, and S. Schuman (eds.). Formal Program Development. IFIP TC2/WG 2.1 State-of-the-Art Report. LNCS 755. Springer-Verlag 1993.
  • H. A. Partsch. Specification and Transformation of Programs. A Formal Approach to Software Development. Springer-Verlag 1990.
  • H. A. Partsch. Requirements Engineering.  Systematische Modellbildung zur Ermittlung der Anforderungen an softwaregestützte Systeme (Arbeitstitel). Springer-Verlag 1998.
  • T. Vullinghs, W. Schulte, Th. Schwinn.  The Design of a Functional GUI Library Using Constructor Classes. PSI'96. In: D. Bjørner, M. Broy, I. Pottosin (eds.), LNCS 1181, Springer-Verlag 1996.

Produkte und Werkzeuge

  • ULTRA
  • TkGofer

Kontaktadresse:

Prof. Dr. H. A. Partsch
Universität Ulm 
Fakultät für Informatik 
Abt. Programmiermethodik und Compilerbau
D-89069 Ulm
Tel.: (0731) 502-4160, Fax: -4162
partschh@informatik.uni-ulm.de