|
Berufungskommission Softwaretechnologie: Vorträge
|
Berufungskommission Softwaretechnologie: Vorträge
|
|
Datum |
2000-05-05 (2000-05-16) |
|
Ort |
Graz |
|
Organisator |
Einladender: o.Univ.Prof.Dr.Dr.h.c.H. Maurer |
|
Land |
Österreich |
| |
|
| Vortrag |
Vortragender |
Kurzfassung |
Am |
| Algebraische Systementwicklung |
Möller Bernhard |
|
2000-05-15 |
| Die Rolle der Modellierung im Software Engineering |
Broy Manfred |
|
2000-05-16 |
| Komponentengestützte Softwaretechnik: Herausforderungen und Ergebnisse |
Krämer Bernd |
|
2000-05-15 |
| Konstruktion und Verwendung von Klassenbibliotheken |
Zimmermann Wolf |
Grosse Softwaresysteme können kaum mit vertretbarem Aufwand komplett neu entwickelt werden. Ein großer Teil wird aus Bibliotheken und anderen Systemen entnommen. Die Verwendung von Programmbibliotheken kann zusätzlich die Produktqualität verbessern: ein Programm, das oft benutzt wird, arbeitet zuverlässiger. Die Bibliothek selbst muss hohen
Qualitätsanforderungen (Korrektheit, Stabilität der Strukturen) genügen und die Benutzung der Bibliothek durch geeignete Werkzeuge unterstützt werden (verständliche Fehlermeldungen, frühe Fehlererkennung, flexibles Zusammensetzen von Komponenten). Der Vortrag diskutiert Massnahmen und Werkzeuge, die mit Erfolg bei der Entwicklung und Verwendung der Klassenbibliothek KARLA (ca. 500 Klassen) eingesetzt wurden.
Zunächst wird diskutiert, welche Probleme bzgl. Korrektheit und Stabilität einer Klassenbibliothek entstehen und mit welchen Massnahmen diese vermieden werden koennen. Anschliessend wird gezeigt, dass bei Verwendung einer statisch typsicheren Programmiersprache durch Wahl geeigneter Bibliotheksstrukturen bereits statisch - also vor der Ausführung - viele fehlerhafte Benutzungen einer Bibliothekskomponente erkannt werden können. Abschliessend wird gezeigt, wie
Bibliothekskomponenten zusammengesteckt und durch Einsatz von Programmgeneratoren an die konkreten Anforderungen angepasst werden können. Dabei ist jeweils eine automatische Konsistenzprüfung möglich, die bereits bei der Generierung Fehlerquellen ausschließt. |
2000-05-05 |
| Korrekte Software |
Giesl Jürgen |
Zusammenfassung:
Um die Sicherheit und Zuverlässigkeit von Programmen zu garantieren, wird eine formale Verifikation benötigt.
Diese Aufgabe ist von hoher praktischer Relevanz in der Softwaretechnologie, da gerade bei verteilten Programmen und bei sicherheitskritischen Anwendungen Untersuchungen zur Korrektheit von grosser Bedeutung sind. Die Durchführung solcher Korrektheitsbeweise ist jedoch im allgemeinen sehr aufwendig - insbesondere bei umfangreichen Algorithmen, wie sie in der Praxis eingesetzt werden. Aus diesem Grund wird versucht, die Aufgabe der Programmanalyse und -verifikation weitgehend zu automatisieren.
Ein zentrales Anliegen beim Entwurf korrekter Software ist der Nachweis der Terminierung. Neben einer kurzen Einführung in
klassische Techniken zur automatischen Terminierungsanalyse wird das darauf aufbauende neu entwickelte "Dependency Pair" Verfahren vorgestellt, das den Einsatzbereich dieser Terminierungstechniken wesentlich erweitert. Unser Terminierungsverfahren wird beispielsweise in einem gemeinsamen Projekt mit Ericsson Telecom für die Behandlung verteilter Prozesse eingesetzt.
Darüber hinaus wird ein Überblick über Werkzeuge zum Nachweis der partiellen Korrektheit gegeben. Diese Systeme untersuchen, ob sich das Programm seiner Spezifikation entsprechend verhält, sofern es terminiert. Insbesondere wird gezeigt, wie automatische Verifikationstools mit Hilfe geeigneter Programmtransformationen für verschiedene Arten von Programmiersprachen und -paradigmen eingesetzt werden können. Hierzu wurde ein Transformationssystem entwickelt, um imperative Programme ohne Verwendung von Schleifeninvarianten rechnergestützt zu verifizieren. |
2000-05-06 |
| Modelling search and evaluating strategies in theorem proving |
Bonacina Maria Paola |
|
2000-05-06 |
| Reliable Practical Software Development Using Abstract State Machines |
Börger Egon |
|
2000-05-06 |
| Schema-Re-Engineering mit Hilfe der VARLET Umgebung |
Schaefer Wilhelm |
Der Einsatz objektorientierter Technologie bei der Entwurfsunterstützung, als objektorientierte Implementierungssprache und als neue Datenbanktechnologie hat inzwischen breite Akzeptanz gefunden. In vielen Anwendungen ergibt sich allerdings das Problem, aus Gründen des Investitionsschutzes diese neue Technologie mit dem Zugriff auf Daten, die in relationalen Systemen vorliegen, zu integrieren. Beispielhafte Anwendungen sind der Aufbau föderierter DB-Systeme oder der Zugriff von mit
JAVA entwickelten Anwendungen auf relationale Datenbanksysteme (z.B. bei der Realisierung von Applikationen für den elektronischen Handel).
Der Vortrag stellt den Paderborner Ansatz zum Schema-Re-Engineering von relationalen Datenbankanwendungen vor. Er beruht auf einer fuzzy-gesteuerten Erkennung von Clichés im Code der relationalen Applikation und der regelbasierten Transformation dieser Clichés in eine objektorientierte Darstellung. Herausragende Merkmale dieses Ansatzes sind die Möglichkeit, diese Regeln, die durch Graphgrammatiken spezifiziert werden, einfach zu ändern und z.B. an firmenspezifische Besonderheiten anzupassen sowie die Möglichkeit inkrementell Änderungen sowohl in der objektorientierten Darstellung als auch in der Darstellung des relationalen Modells vorzunehmen. Die VARLET(Verified Analysis and Reengineering of Database
Systems using Equivalence Transformations)-Umgebung sorgt aufgrund der spezifizierten Regeln für sofortige und automatische Konsistenz zwischen beiden Repräsentationen. |
2000-05-05 |
| UML fundiert |
Breu Ruth |
Kurzfassung:
Die Unified Modeling Language (UML) ist ein Industriestandard zur objektorientierten Modellierung von Systemen. Trotz vielfältiger Anstrengungen sind heute viele Konzepte dieser Sprache noch nicht völlig verstanden, besonders was das Zusammenspiel und den methodischen Einsatz ihrer graphischen Beschreibungstechniken betrifft.
Dieser Vortrag stellt einen semantisch fundierten Entwurfsrahmen für den objektorientierten Software-Entwurf mit dem Anwendungsschwerpunkt verteilter Informationssysteme vor.
Nach einer kurzen Einführung in die Basiskonzepte und -techniken objektorientierter Modellierung mit der UML geht der Vortrag auf die Methodik der Anwendungsfaelle (engl. use cases) und deren Umsetzung auf Ebene der UML-Beschreibungstechniken ein. Im Schlussteil des Vortrags wird ein semantischer Rahmen vorgestellt, der eine abstrakte Gesamtsicht kommunizierender Objekte beschreibt. Durch ihre Einbettung in diese Gesamtsicht werden die Beschreibungstechniken nicht nur in grundlegender Weise mit dem Objektbegriff integriert, sondern es wird auch ein Rahmen geschaffen, in dem das Zusammenspiel unterschiedlicher Techniken untersucht werden kann. Fragestellungen, die in diesem Zusammenhang untersucht wurden, sind z.B. die Rolle von Sequenz- und Zustandsdiagrammen bei der Spezifikation dynamischen Objektverhaltens oder die Interpretation von Invarianten im Kontext nebenläufig agierender Objekte. |
2000-05-05 |
|
|
