Melden Sie sich hier an, um auf Kommentare und die Whitepaper-Datenbank zugreifen zu können.

Kein Log-In? Dann jetzt kostenlos registrieren.

Falls Sie Ihr Passwort vergessen haben, können Sie es hier per E-Mail anfordern.

Der Zugang zur Reseller Only!-Community ist registrierten Fachhändlern, Systemhäusern und Dienstleistern vorbehalten.

Registrieren Sie sich hier, um Zugang zu diesem Bereich zu beantragen. Die Freigabe Ihres Zugangs erfolgt nach Prüfung Ihrer Anmeldung durch die Redaktion.

08.03.1991 - 

Dem englischen Beispiel folgen (Teil 1)

Die Anwender verschlafen den Trend zu " Safer Software"

08.03.1991

Während in England mit den "Formal Methods" eine Revolution des Software-Engineering in Gestalt einer engen und erfolgreichen Zusammenarbeit zwischen Universität und Industrie begonnen hat, ist die Kluft zwischen industrieller Praxis und den Hochschulen hierzulande größer denn je. Ein neues Qualitätsbewußtsein in der Software-Entwicklung, so Martin Weigele und Jan Peleska*, wird diese Zusammenarbeit fordern.

Die immer komplexen werdenden Problemstellungen sind nur durch den Einsatz exakter und zugleich praxisgerechter Entwurfsmethoden lösbar, die aus der Verbindung herkömmlicher Software-Entwicklung und formaler Verifikation jüngst entstanden sind. Freilich hat Qualität auch ihren Preis, der sich aber bekanntlich auf Dauer auszahlt.

Die Computerbranche - insbesondere die Software-Entwicklung - ist von ständig wachsenden Ansprüchen gekennzeichnet. In merkwürdigem Kontrast dazu stehen die Entwicklungsmethoden, wie sie nach wie vor in der Industrie eingesetzt werden. Besonders alarmierend ist die Tatsache, daß ein Großteil der Branche besonders die teueren betriebswirtschaftlich orientierten DV-Beratungen - noch immer Softwaretechniken aus den 50er Jahren einsetzen.

Dabei könnten spätestens seit den 70er Jahren Modularisierungs- und Strukturierungstechniken und unterstützende Programmiersprachen benutzt werden. Ebenso wird offensichtlich die nächste revolutionäre Entwicklung in der Softwaretechnologie verschlangen Die Entwicklung von Safer Software, wie sie in Großbritannien als erfolgreiche Kooperation von Industrie und Universität vorangetrieben wird.

Wer ein Auto kauft, dem leuchtet ein, daß er für ein qualitativ hochwertiges und sicheres Fahrzeug mehr bezahlen muß. Nicht ohne Grund bevorzugen zum Beispiel Taxifahrer bestimmte Pkw-Typen. Im Bereich der Software fehlt ein vergleichbares Bewußtsein. Das wird sich spätestens dann rächen, wenn durch leichtsinniges Weiterwursteln Dinosaurier-artige Systeme entstanden sind, die kein Mensch mehr beherrschen kann. Noch immer haben es die DV-Verantwortlichen leichter, einen Manager davon zu überzeugen, Millionenbeträge für teure Hardware auszugeben, als ein paar hunderttausend Mark für bessere Software zu veranschlagen.

Es ist erschütternd zu sehen, welch veraltete Systeme heute im Alltag eingesetzt werden, und wie wenig Anwender sich darüber im klaren sind, an welch seidenem Faden das Funktionieren hängt. Nicht selten sogar stoßen Kritiker auf Unverständnis und Arroganz, ganz nach dem Motto "Was nicht sein kann, das darf nicht sein!". Dabei kann ein Fehler nicht nur Milliardenbeträge kosten, er kann auch den Absturz eines Flugzeuges verursachen und Menschen in Gefahr bringen. Wer hier nicht alle Möglichkeiten der Verbesserung ausschöpft, handelt unverantwortlich.

Das Konzept der Safer Software ist nichts anderes als ein Konstruktionsplan für Software, der dem Vorgehen des Architekten beim Hausbau entspricht: sorgfältige Planung und Umsetzung der Wünsche des Bauherrn, um zu vermeiden, daß die Toilette nicht versehentlich vergessen oder die Haustür im fünften Stock eingebaut wird, aber auch erforderliche Berechnungen, die garantieren, daß das Haus hinterher nicht zusammenstürzt.

Um solche Ereignisse auszuschließen, werden traditionelle Methoden des Software-Engineering, wie Strukturierung, schrittweise Verfeinerung und Top-Down-Zerlegung mit den Methoden der mathematischen Programmverifikation verbunden. So können einerseits reale Probleme mit Methoden der Programmverifikation angefaßt werden, um die Korrektheit von Programmen durch mathematische Beweise zu verifizieren. Andererseits läßt sich die langjährige Erfahrung von Methoden des Software-Engineering in einer gelungenen Verbindung von Theorie und Praxis nutzen.

Safer Software entsteht also aus der Verbindung von zwei Technologien, die in der Informatik für sich genommen seit längerem bekannt sind. Die Vorgehensweise wird im folgenden noch genauer erläutert und mit dem Begriff "Formales Software-Engineering" (im Englischen "Formal Methods") bezeichnet. Korrektheitsbeweise werden dabei mit der Methode der schrittweisen Verfeinerung

kombiniert.

Fehlerfreie und somit ausfallsichere Softwaresysteme werden wichtiger, je weiter der Grad der Computerisierung fortschreitet. Systeme mit hoher Verfügbarkeit, Non-Stop-Systeme, schwer testbare Systeme und sicherheitskritische Anwendungen sind typische Kandidaten für Safer Software. Immer wieder hört man von elektronischen Einbrüchen in sensible Datenbestände, wie sie zum Beispiel bei Banken vorliegen.

Oft werden den Tätern Schweigegelder angeboten, damit der Skandal erst gar nicht an die Öffentlichkeit dringt, weil sonst der Ruf des betroffenen Unternehmens Schaden nehmen könnte. Noch offensichtlicher ist der Bedarf bei der "mission critical software" - zum Beispiel in Kraftwerken, in der Logistik von Verkehrssystemen, beim Fliegen oder in der Raumfahrt, wo Softwarefehler den Totalausfall verursachen und Menschenleben gefährden können.

Aber auch bei alltäglicher Software ist ein höheres Qualitätsbewußtsein dringend nötig, da sonst die Systeme, die aus fehlerhaften Bausteinen zusammengebaut werden, im Laufe der Zeit praktisch nicht mehr beherrschbar sind. Da tickt eine Zeitbombe, aus der jederzeit ein riesiger wirtschaftlicher Schaden entstehen kann. Die EG-Kommission setzt schon seit einiger Zeit in Ihrer Technologiepolitik auf die Formal Methods und auch auf Bundesebene, so ist zu hören, soll eine oberste Behörde eingerichtet werden, die sich mit derlei Fragen beschäftigt.

Wie unterscheidet sich nun Formales Software-Engineering (FSE) von der herkömmlichen Vorgehensweise? Die Idee ist im Grunde recht einfach: Die aus der Praxis bekannten Verfahrensweisen werden in einen mathematischen Rahmen übertragen. Dieses Verfahren hat bereits Anfang des Jahrhunderts der Physik und in der Folge den Ingenieurwissenschaften zu neuen Erfolgen verholfen.

Wenig Zeit und wenig Aufwand nötig

Mit relativ einfachen mathematischen Hilfsmitteln, wie dem Einsatz von Mengenlehre mit Relationen und Funktionen, werden die Benutzerwünsche als Aussagen in der Mathematischen Logik (Prädikatenlogik) beschrieben. Mathematische Logik ist aber im Grunde nichts anderes als die Bereitstellung formaler Hilfsmittel für den gesunden Menschenverstand.

Der Vorteil besteht vor allem darin, daß nicht erst viel Zeit und Aufwand in das Erlernen einer "unnatürlichen" Logik (mehrwertige Logik, temporale Logik, Klausellogik) investiert werden muß. Man kann sich von vornherein weitgehend auf das eigentliche Verifikationsproblem konzentrieren. Damit das Ganze auch bei umfangreichen Problemstellungen praktisch angewandt werden kann, ist nun die Verbindung dieser Vorgehensweise mit aus dem Software-Engineering bekannten Methoden erforderlich, wie zum Beispiel Methoden der Strukturierung und Top-Down-Zerlegung.

Problem muß exakt beschrieben werden

Ausgangspunkt ist dabei eine Beschreibung, die die Komponenten eines zu modellierenden Systems auf einer abstrakten Beschreibungsebene in strukturierter Weise modelliert. Dabei spielen Implementierungs-Betrachtungen zunächst keine Rolle, es wird also unabhängig von der später zu verwendenden Hard- oder Softwareumgebung eine möglichst exakte Problembeschreibung und Zerlegung in Komponenten angefertigt.

Diesen Komponenten können dann die entsprechenden mathematischen Objekte in Form von Prädikaten problemlos zugeordnet werden. Je nach Anwendungsgebiet stehen hierfür verschiedene Kalküle bereit. Einerseits kann das Verhalten des Systems als Folge beziehungsweise als "Spur" von möglichen Ereignissen (englisch: traces) beschrieben werden. Diese Art der Modellierung ist vor allem für Problemstellungen mit gewünschter Parallelverarbeitung hilfreich.

Andererseits kann die Beschreibung durch Angabe von erlaubten beziehungsweise verbotenen Zustandsübergängen des Systems geschehen. Anhand der Prädikate läßt sich die Schlüssigkeit (beziehungsweise Konsistenz) der gewonnenen Spezifikation sozusagen rechnerisch mit Hilfe der Logik überprüfen.

Entscheidend ist dabei, daß diese Überprüfung, anders als bei der klassischen Programmverifikation, zunächst einmal auf der abstrakten Ebene der Spezifikation erfolgt. Das ermöglicht, auch beim Nachweis der Korrektheit, nicht von vornherein auf zahllose Implementierungsdetails eingehen zu müssen.

Sowohl die Spurenbeschreibung als auch die Angabe von Zustandsübergängen führt dazu, daß die so gewonnene abstrakte Spezifikation eine Implementierung auf einem bestimmten Rechnersystem mit all seinen spezifischen Bedingungen und Einschränkungen nach sich zieht. Dieses Ziel wird mit der klassischen Methode der schrittweisen Verfeinerung erreicht, besser bekannt unter dem englischen "Stepwise Refinement".

Schritt um Schritt wird die vom Kunden gewünschte Funktionalität von einer abstrakten in eine immer konkretere Beschreibung mit Implementierungsdetails bis hin zum Programmcode umgewandelt. Der große Vorteil dieses Procedere liegt darin, daß für eine ursprünglich als korrekt bewiesene Spezifikation nur noch die Richtigkeit der einzelnen Verfeinerungsschritte zu beweisen ist. So ist es möglich, den Wust an Details in den Griff zu bekommen, der lange Zeit den Einsatz von Programm-Verifikationsmethoden in der Praxis verhinderte, weil diese direkt auf der Ebene des fertigen Programms eingesetzt wurden.

Auch ist eine ganz "normale" Top-Down-Zerlegung in diese Vorgehensweise integriert (siehe Abbildung 2). Die anfallenden Beweise sind meistens relativ einfach. Eher besteht das Problem der Menge, das jedoch durch den Einsatz der Strukturierungs- und Verfeinerungsstrategien bewältigt werden kann: Die Strukturierung des Problems spiegelt sich in den Beweisen wider. Bei diesen können dann auch automatische Beweissysteme oder sogenannte Beweisassistenten zur Überprüfung der einzelnen Schritte nutzbringend eingesetzt werden.

Ein weiteres Problem ist die Ablehnung mathematischer Beweise aufgrund mangelnden Verständnisses und unangenehmer Erinnerung an die Schulzeit. Hier kann durch zusätzliche Erklärungen, wie nachfolgend beschrieben, zum Teil Abhilfe geschaffen werden. Andererseits bedarf es der Aufklärung. Welchen Nutzen hat für den Kunden ein eindrucksvoller Test? Er mag in wenigen Spezialfällen zwar das gewünschte Ergebnis liefern, im allgemeinen können Tests aber immer nur die "Anwesenheit einzelner Fehler" zeigen. Bei einem hinreichend komplexen System ist es meistens gar nicht mehr möglich, alle möglichen Fälle zu testen.

Hingegen kann ein Beweis die vollständige "Abwesenheit" von Fehlern garantieren. Schließlich scheint der Gedanke interessant, daß solche Verifikationsaufgaben auch von unabhängigen Prüfstellen übernommen werden können.

Das zentrale Problem des Software-Engineering ist auch beim Einsatz Formaler Methoden die korrekte Abbildung des Benutzerwunsches. Während für den Entwickler die Möglichkeit hilfreich ist, seinen Systementwurf auf Korrektheit, beziehungsweise Konsistenz zu überprüfen, bleibt doch das Problem, die Rückkopplung mit dem Kundenwunsch herzustellen. Freilich unterscheiden sich Formale Spezifikationen in diesem Punkt nicht von Programmen. Beim Bestreben, ein möglichst eindeutiges Pflichtenheft zu erhalten, weisen Formale Spezifikationen jedoch auch in dieser Hinsicht einige Vorzüge auf. Durch den Verzicht auf Implementierungsdetails in der Ausgangsspezifikation ist diese von vornherein der Betrachtungsebene des Benutzers recht nahe.

Um eine Diskussionsbasis mit dem Auftraggeber zu haben, ist es möglich, formale Spezifikationen mit den üblichen Methoden darzustellen. Diese lassen sich in geeignete Schaubilder und Diagramme übersetzen. Umgekehrt kann, wie schon erwähnt, den informellen Beschreibungen eine formale Bedeutung gegeben werden. Der Vorteil gegenüber herkömmlichen Schaubildern besteht darin, daß die Symbole eine stärker eingeschränkte, dafür aber exakte Bedeutung (oder Semantik) für den Entwickler haben.

Der Kunde muß diese Symbole im Detail nicht kennen, er erhält eine Veranschaulichung des dahinterstehenden mathematischen Modells. Auf diese Weise entstehen zwei Sichten der Spezifikation, eine Kundensicht und eine Entwicklersicht. Beide repräsentieren den Kundenwunsch.

Weiterhin lassen sich einmal gewonnene formale Spezifikationen wieder in natürliche Sprache zurückübersetzen. Die entstehenden Beschreibungen sind durch ihre Entstehungsgeschichte wesentlich präziser als das natürlichsprachliche Ausgangsdokument und so für den Entwickler hilfreicher.

Vor allem können formale Spezifikationen dazu dienen, logische Schlüsse aus ihnen zu ziehen. Der Kunde kann befragt werden: "Du hast mir diese zwei Eigenschaften vorgeschrieben. Ich kann daraus beweisen, daß das System dann auch noch diese dritte Eigenschaft haben muß. Ist das wirklich erwünscht?" Anhand der formalen Spezifikation kann also ein Fragenkatalog mit Konsequenzen des spezifizierten Systems erstellt werden, die in den ursprünglichen Benutzerwünschen nicht enthalten waren.

Der Benutzer kann dann diesen Fragenkatalog durcharbeiten. Auf diese Weise läßt sich feststellen, ob er sich wirklich über die möglichen Folgen aus seinen Forderungen im klaren war. Sind die Folgen nicht mit seinen Wünschen vereinbar, so deutet dies auf die Unverträglichkeit von Benutzerwünschen hin. Zur Auflösung dieses Konflikts kann eine entsprechende Entscheidung getroffen werden.

Die Tatsache, daß der Benutzer formale Spezifikationen meistens nicht versteht, ist somit kein echter Nachteil, da diese mit informellen Hilfsmitteln gut verständlich gemacht werden können. Ist andererseits ein Auftraggeber in der Lage, seine Wünsche anhand des Programmcodes deutlich zu machen, so wird er unter Umständen auch fähig sein, sich mit einer solchen Spezifikationssprache zu befassen. Im Bereich der Telekommunikation dienen ähnliche Spezifikationssprachen teilweise bereits zur Abfassung von Pflichtenheften, weil die Probleme anders gar nicht mehr in den Griff zu bekommen sind.

Ein wichtiger Punkt ist die Animation von Spezifikationen in Form eines "Rapid Prototype". Ein solcher Prototyp ist in besonderem Maße geeignet, dem Kunden das Ergebnis seiner Wünsche "zum Anfassen" zu präsentieren. Im Bereich der Parallelverarbeitung und der Kommunikation sequentieller Prozesse bietet beispielsweise die Spezifikationssprache CSP die Möglichkeit des relativ raschen Übergangs zu einer Implementierung mit Hilfe von Occam, die als eine Teilsprache in CSP enthalten und auf Transputern realisiert ist.

Große und komplexe Software-Systeme komplett zu verifizieren mag zunächst hoffnungslos erscheinen. So stellt sich die Frage, inwieweit es möglich ist, aus der Verifikation von Subsystemen einen Nutzen zu ziehen. Da Programme diskrete Vorgänge beschreiben, genügt in der Regel ein winziger Fehler in einem Teil, um das gesamte Produkt unbrauchbar zu machen. Dies bedeutet, daß grundsätzlich das schwächste Glied in der Kette ausschlaggebend ist für die Zuverlässigkeit des gesamten Systems.

(wird fortgesetzt)

Safer Software - Computerprogramme, die zuverlässiger funktionieren Spezifikation Spezifikation - Beschreibung, was gebaut werden soll.

Formale Spezifikation - Mathematische Form dieser Beschreibung.

Verifikation - Beweis von Eigenschaften von Programmen.

Software-Engineering - Erstellen von Spezifikationen aus Benutzerwünschen und deren Umsetzung in Computerprogramme.

Formales

Software-Engineering - Software-Engineering mit mathematischen Hilfsmitteln.

Design - Umsetzen des Was der Spezifikation in das Wie der Implementierung.

Stepwise Refinement - Methode des Design.

Fehlertolerantes System - Ein System, das auftretende Fehler abfangen kann.