TU München
Technische Universität München
Forschungs- und Lehreinheit Informatik IV
und FORSOFT
Methodik der Programm- und Systementwicklung
Prof. Dr. Manfred Broy, Ordinarius (http://wwwbroy.informatik.tu-muenchen.de/~broy/)
Prof. Tobias Nipkow, Ph.D., Extraordinarius (http://wwwbroy.informatik.tu-muenchen.de/~nipkow/)
Prof. Dr.-Ing. Ernst Denert, Honorarprofessor (http://wwwbroy.informatik.tu-muenchen.de/~denert/)
Prof. Dr. Karl-Rudolf Moll, Honorarprofessor (http://www4.informatik.tu-muenchen.de/~moll/)
Arbeitsschwerpunkte
Methodik der Softwareentwicklung, Modellierungstechniken und ihre Semantik, Spezifikations- und Programmiersprachen (12, 10, 11), insbes.
- Techniken für
- das Requirements Engineering,
- die komponentenorientierte Architekturbeschreibung,
- das Qualitätsmanagement (incl. maschinelles Beweisen) und
- die funktionale und objektorientierte Programmierung.
- Anwendungsgebiete
- eingebettete Systeme,
- Informationssysteme und
- verteilte Systeme.
- Unterstützung durch Entwicklungswerkzeuge (Tools).
- Kooperationsprojekte mit der Industrie.
Projekte
BEQUEST - Beschreibungstechniken und formale Qualitätssicherung für eingebettete Systeme, DFG-Projekt Br 887/9-1 im Rahmen des Schwerpunktprogramms ``Entwurf und Entwurfsmethodik eingebetteter Systeme''.
Ziel ist die Entwicklung von Beschreibungstechniken, die wissenschaftlich und mathematisch fundiert sind und somit eine formale, maschinengestützte Verifikation sicherheitsrelevanter Systemeigenschaften erlauben. Selbstverständlich müssen die Beschreibungstechniken genügend ausdrucksmächtig sein und auf die Perzeptionsgewohnheiten klassischer Anwendungsfelder Rücksicht nehmen. Die erforderliche Grundlagenarbeit wird durch eine Konzeption und prototypische Realisierung für eine Werkzeugunterstützung ergänzt, und mit Fallstudien erprobt.
DEDUKTION - Deduktion für objektorientierte Programmiersprachen, Teilvorhaben im DFG-Schwerpunktprogramm ``Deduktion''
Untersucht wird der Einsatz deduktiver Methoden im Software- und Systementwicklungsprozess. Aktuell steht die Modellierung von Java im Vordergrund Bisher wurden abstrakte Syntax, Typsystem und operationale Semantik von Java, sowie die Semantik der Java Virtual Machine formalisiert, und bewiesen, daß diese formalisierte Teilsprache typsicher ist. Zur Zeit wird der Bytecode Verifier spezifiziert, um Eigenschaften über ihn zu beweisen. Es ist geplant, Erweiterungen von Java, z.B.\ um parametrisierte Typen, und die Korrektheit von Java-Übersetzern formal zu analysieren. Dazu wird der Theorembeweiser Isabelle, insbesondere die Instantiierung Isabelle/HOL für Logik höherer Stufe, verwendet.
Methodik des Entwurfs verteilter Systeme, Teilprojekt A6 des SFB 342, ``Methoden und Werkzeuge für die Nutzung paralleler Rechnerarchitekturen''
FOCUS ist eine Methodik zur formalen Spezifikation und Entwicklung verteilter, reaktiver Systeme (6). Aktuelle und für die nächste Zukunft geplante Arbeiten befassen sich mit einer Methodik der spezifikationsbasierten Systementwicklung, der werkzeuggestützten Verifikation und Validierung und dem Einsatz von FOCUS in spezifischen Anwendungsbereichen.
Bayerische Forschungsverbund Software-Engineering
Der Bayerische Forschungsverbund Software-Engineering (FORSOFT) ist eine enge interdisziplinäre Kooperation zwischen Wissenschaft und Praxis sowie Technik und Anwendung. Er nahm im Februar 1997 seine Arbeit auf und wird für einen Zeitraum von drei Jahren durch die Bayerische Forschungsstiftung finanziert sowie von zahlreichen Industriepartnern. 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 (1). Die Teilprojekte A1 (7), A2, A3, A4, C3 (8) und Zwerden am Lehrstuhl IV durchgeführt.
KORSYS - Korrekte Software für sicherheitskritische Systeme, Kooperation mit BMW, ESG, OFFIS (Oldenburg) und Siemens ZT
Projektziel ist die Schaffung eines Baukastensystems von Unterstützungswerkzeugen, von an die Praxis angepaßten Beschreibungsverfahren und einer spezifisch ausgebauten Methodik für die Anwendung im Bereich verteilter, reaktiver und zeitkritischer Systeme (3).
QUEST - Kooperation mit DFKI in Saarbrücken und Daimler Benz Berlin, im Auftrag des BSI
Ziel von QUEST ist es, formale Methoden so in den Entwicklungsprozeß zu integrieren, daß sicherheitskritische Systeme und Komponenten mit beweisbaren Eigenschaften entwickelt werden können. Die Kombination von informellen (d.h. ohne Anwendung formaler Methoden), semiformalen und formalen Entwicklungen ist für QUEST von besonderer Bedeutung.
SYSLAB - Forschungslabor für Software- und Systementwicklung, Finanzierung aus Leibniz-Mitteln DFG, Kooperationspartner: Siemens ZT, Siemens ÖN, SNI
Das Ziel des SysLab-Projekts ist die Entwicklung einer mathematisch fundierten Software-Entwicklungsmethodik für verteilte, interaktive objektorientierte Systeme, angelehnt an UML (4). Dabei steht der Zielbereich betrieblicher Informationssysteme mit großem, stark strukturiertem Datenraum, einer graphischen Schnittstelle zu Benutzern, und einem verteilten Netz von Anwendungen im Vordergrund.
TYPES - Types for Proofs and Programs, Teilprojekt des gleichnamigen ESPRIT BRA-Projekts
Dieses Projekt befaßt sich mit den logischen und typtheoretischen Grundlagen formaler mathematischer Beweise und deren Anwendungen in der Informatik unter Betrachtung der Entwicklung mächtiger logischer Formalismen, der Implementierung von interaktiven Beweisunterstützungssystemen für diese Formalismen, und der Anwendung der genannten Theorien und Werkzeuge auf konkrete Probleme in der Informatik (5).
Veröffentlichungen
- M. Broy and H. Ehler and B. Paech and V. Thurner, Innovation durch Kooperation im Software-Engineering, Informatik'97, GI-Jahrestagung, M. Jarke and K. Pasedach and K. Pohl, Informatik aktuell, 503-504, 1997.
- T. Nipkow and D. von Oheimb, Java is Type-Safe -- Definitely, Proc. 25th ACM Symp. Principles of Programming Languages, ACM Press, 1998, to appear.
- T. Stauner and O. Müller and M. Fuchs, Using HyTech to Verify an Automotive Control System, Proc. Hybrid and Real-Time Systems, Grenoble, March 26-28, LNCS 1201, Springer, 139-154, 1997.
- R. Breu and U. Hinkel and C. Hofmann and C. Klein and B. Paech and B. Rumpe and V. Thurner, Towards a Formalization of the Unified Modeling Language, ECOOP, LNCS 1241, 344-366, 1997.
- W. Naraschewski and T. Nipkow, Type Inference Verified: Algorithm W in Isabelle/HOL, Proc. Int. Workshop TYPES'96, C. Paulin-Mohring, Springer, LNCS, 1997.
- M. Broy and M. Breitling and M. Fuchs and T. F. Gritzner and B. Schätz and K. Spies and K. Stølen, Summary of Case Studies in FOCUS - Part I and II, TUM-I9423, TUM-I9740, Technische Universität München, 1994, 1997.
- K. Bergner and A. Rausch and M. Sihling, Using UML for Modeling a Distributed Java Application, TUM-I9735, Technische Univerität München, 1997.
- P. Scholz, A Refinement Calculus for Statecharts, ETAPS/FASE'98, Lisbon (Portugal), March 30 - April 03, 1998, to appear.
- F. Huber and B. Schätz and G. Einert, Consistent Graphical Specification of Distributed Systems, FME '97, LNCS 1313, 122-141, Springer, J. Fitzgerald and C. B. Jones and P. Lucas, 1997.
- M. Broy, Mathematik des Software-Engineering, Highlights aus der Informatik, Springer, I. Wegener, 229-252, 1996.
- M. Broy, Towards a Mathematical Concept of a Component and its Use, Software - Concepts and Tools, 18, 137-148, 1997.
- M. Broy, Mathematical System Models as a Basis of Software Engineering, Computer Science Today, LNCS 1000, Springer, J. van Leeuwen, 292-306, 1995.
Produkte und Werkzeuge
AutoFocus - Verteilte Systeme
Mit AutoFocus wird basierend auf formalen Methoden der Systementwicklung ein Werkzeugprototyp entwickelt, der den Spezifikationsentwurf durch
- integrierte hierarchische Beschreibungsmittel,
- verteilte und plattformunabhängige Entwicklung und
- Versionsverwaltung und Sperrkonzepte
unterstützt (9).
Kontaktadresse:
Technische Universität München
Forschungs- und Lehreinheit Informatik IV
und FORSOFT Methodik der Programm- und Systementwicklung
Arcisstr. 21, 80290 München
www4.informatik.tu-muenchen.de
Prof. Dr. Manfred Broy, Ordinarius (http://wwwbroy.informatik.tu-muenchen.de/~broy/)
Tel.: (089) 2105-8161, Fax: -8183
broy@informatik.tu-muenchen.de
Prof. Tobias Nipkow, Ph. D., Extraordinarius (http://wwwbroy.informatik.tu-muenchen.de/~nipkow/)
Tel.: (089) 289-22690
nipkow@informatik.tu-muenchen.de
Prof. Dr.-Ing. Ernst Denert, Honorarprofessor (http://wwwbroy.informatik.tu-muenchen.de/~denert/)
Tel.: (089) 289-28162
Prof. Dr. Karl-Rudolf Moll, Honorarprofessor (http://www4.informatik.tu-muenchen.de/~moll/)
Tel.: (089) 9244-4253, Fax: 4448
krm@mail.Hypo.de