Nehmen wir mal an, ich habe in C eine Funktion geschrieben und muß nun beweisen, daß sie korrekt funktioniert. Zum Beispiel, weil sie die Impulsdauer für einen Herzschrittmacher berechnet oder den Querruderwinkel an einem Flugzeug. Also, ich tue das nicht wirklich, sonst hätte ich hoffentlich Ahnung davon. Mich interessiert nur, wie so etwas in der Praxis abläuft. Ich habe also einen Quelltext geschrieben mit sagen wir zwei Parametern zur Übergabe und einem Rückgabewert. Den lasse ich übersetzen und bekomme Objektcode bzw. Maschinencode. Wie weise ich jetzt nach, daß meine Funktion - sich nicht in einer Endlosschleife verirrt - nicht Speicher auffrisst, bis der Rechner abschmiert - für alle Kombinationen von Eingangswerten ein korrektes Ergebnis liefert - nicht noch irgendwo im Speicher was macht, wo sie nichts machen soll - sich bei ungültigen Eingangswerten definiert verhält ???
Es ist nicht möglich zu beweisen, dass ein Algorithmus terminiert.
("Halteproblem")
Mark Brandis schrieb: > Es ist nicht möglich zu beweisen, dass ein Algorithmus terminiert. > ("Halteproblem") Diese Aussage stimmt so nicht. Die Aussage des Halteproblems lautet: Es ist nicht möglich, für jeden beliebigen Algorithmus ein Verfahren zu finden, welches entscheidet ob der Algorithmus zu einem Ende kommt. Knackpunkt ist "für jeden beliebigen Algorithmus". Daraus folgt aber nicht, dass ein Korrektheitsbeweis für einzelne Algorithmen bzw. eine ganz Klasse von Algorithmen nicht möglich ist. Er muss nur beweisen, dass sein Programm, sein Algorithmus einen Satz von Eingangsdaten in einen Satz von Ausgangsdaten überführt, welche bestimmte Eigenschaften aufweisen. Allerdings sind solche Beweise mühsam und langwierig. Wir haben das mal im ersten Semester gemacht. Um einen eher simplen Bubblesort (=5-Zeiler) formal zu beweisen, hat es immerhin 2 volle Seiten DIN-A4 gebraucht. Alles beginnt damit, dass man zunächst die exakten Eigenschaften der Eingangs- und Ausgangsdaten festlegt.
...okay und hier der Rest ;-)
(war gerade beim Editieren)
Es ist nicht möglich zu beweisen, dass ein Algorithmus generell
terminiert. ("Halteproblem")
Ansonsten gilt:
-Speicherverbrauch zur Laufzeit kann man beim Debuggen testen
-für eine begrenzte Anzahl an Eingangsvariablen kann man alle
(relevanten) Werte im Modultest mal durchjagen und aufzeichnen, was am
Ausgang herauskommt (zum Beispiel mit CUnit,
http://cunit.sourceforge.net/)
-Hundertprozentig fehlerfreie Software gibt es nicht! Der Testaufwand
wird beliebig hoch, bevor die Software fertig wird ist der Kunde
verstorben.
Gib mir ein Schnipsel Assembler, und ich sage dir, ob er für alle Eingabewerte terminiert. "Beweis durch Hinschauen".
Oliver Döring schrieb: > Gib mir ein Schnipsel Assembler, und ich sage dir, ob er für alle > Eingabewerte terminiert. "Beweis durch Hinschauen". Ich geb Dir paar tausend Zeilen. Deal?
Nein. Brich dein Problem in ein paar sinvolle Teilprobleme herunter und gehe die erstmal einzeln an. Übrigens: Bei wirklich sicherheitskritischen Anwendungen muß man nicht unbedingt rechnen lassen. Nehmen wir an, du hast als Eingabe ein 16-Bit-Sample von einem A/D-Wandler und willst als Ausgabe mit einer beliebig komplizierten Berechnung einen "double"-Wert zurückgeben. Dann bau dir eine Tabelle der Größe 2^16 * (2 + 8) = 640 kByte. Das Nachschauen in einer Tabelle ist einfach zu implementieren und zu "beweisen". Die 640 kByte für die Tabelle tun auf einem >8 bit Embedded System meistens nicht besonders weh. Schmerzhafter wäre es dagegen, die Korrektheit deines Algorithmus, die Implementierung in C und vor allem die deines Compilers zu beweisen. Natürlich muß die Berechnungsformel an sich erstmal stimmen, aber das ist ein anderes Problem.
Bei sicherheitskritischen Flugzeugteilen sind bestimmte Programmiertechniken verboten (Rekursion, Schleifen mit nicht-definierter Durchlaufanzahl) und werden bestimmte worst-case Untersuchungen gemacht (Laufzeit bei voller Interrupt-Auslastung etc.), und natürlich muss alles im Quelltext offenliegen. Näheres zu den Vorschriften in FAA Dokument DO-178B Level A Damit kann man leichter prüfen, aber natürlich hilft das alles nichts, wenn der Prozessor z.B. wegen kosmischer Strahlung Unsinn baut. Beweisen geht also immer nur im betrachteten Scope, und da sollte man den disassemblierten Maschinencode betrachten und nicht den C-Quelltext. Das spricht für kleine Programme :-) fasse dich also kurz. Eine Aufteilung in sicherheitsrelevantes und 'schmückendes Beiwerk' ist nützlich.
> Natürlich muß die Berechnungsformel an sich erstmal stimmen, aber > das ist ein anderes Problem. Das ist eigentlich kein anderes Problem, sondern nur eine Verlagerung des ursprünglichen Problems auf ein anderes System. Damit du beweisen kannst, daß dein Tabellen-Lookup immer das richtige Ergebnis liefert, mußt du nämlich erstmal beweisen, daß das Programm zur Berechnung der Tabelle fehlerfrei ist.
War bei Flugzeug-Systemen nicht auch mal was, dass die Teile, die mehrfach vorhanden sind, nicht mit der gleichen Software ausgestattet sein dürfen? Glaube, es darf sogar nicht mal der gleiche Programmierer sein.
> Das ist eigentlich kein anderes Problem, sondern nur eine Verlagerung > des ursprünglichen Problems auf ein anderes System. Damit du beweisen > kannst, daß dein Tabellen-Lookup immer das richtige Ergebnis liefert, > mußt du nämlich erstmal beweisen, daß das Programm zur Berechnung der > Tabelle fehlerfrei ist. Die Frage ist, um welches System herum die Grenze der Zulassung gezogen wird. Wenn ich mit komplexen Teilproblemen aus dieser Grenze rauskomme, wird es viel einfacher. Da lasse ich Excel rechnen, Open Office und zum Schluß ein C-Programm auf dem PC. Wenn die alle das gleiche ausspucken, wird's wohl ungefähr stimmen. Oder man lässt sich die Tabelle gleich vom Kunden absegnen.
> War bei Flugzeug-Systemen nicht auch mal was, dass die Teile, die > mehrfach vorhanden sind, nicht mit der gleichen Software ausgestattet > sein dürfen? Es wurde zumindest beim A320, dem ersten zivilen Flugzeug mit rein elektronischer Ansteuerung der meisten Ruder, so gemacht. Drei verschiedene Rechnerarchitekturen, drei verschiedene Compiler und Programmiersprachen, drei verschiedene Zulieferer. Im normalen Betrieb können zwei Rechner den dritten überstimmen, wenn es Abweichungen gibt. Das gilt jetzt für die Flugsteuerung. Wenn der A320 drei Funkgeräte mit sich rumschleppt, werden das drei gleiche mit dreimal der gleichen Software sein. Da könnte ich eine lustige Geschichte zu erzählen ;) > Glaube, es darf sogar nicht mal der gleiche Programmierer sein. Generell wird in der Luftfahrt und anderen sicherheitskritischen Bereichen mit "personeller Redundanz" gearbeitet. Einer schreibt, der andere kontrolliert, der dritte prüft, ob nach Qualitätsmanagement-Handbuch geschrieben und kontrolliert wurde ;)
Diese Redundanzen ergeben aber keinen Beweis der Korrektheit, sondern verringern nur die Fehlerwahrscheinlichkeit. Das ist ein kleiner, aber feiner Unterschied!
Ich vermute einfach mal, daß der Beweis der Korrektheit des erzeugten Maschinencodes nicht gefordert bzw. nicht möglich war, so daß als Alternative dreifache Redundanz mit "dissimilarity" eingebaut wurde.
Es gibt ja ganz unterschiedliche Fehlerarten, und dementsprechend sind
auch die Strategien unterschiedlich, ihr Auftreten zu verringern bze.
ihr Auswirkung beim Auftreten gering zu halten/einzugrenzen.
1) Softwarefehler
1.a) Designfehler/konzeptionelle Fehler
1.b) Flüchtigkeitsfehler
1.c) Nicht aufgedeckte Fehler durch mangelnde Qualitätssucherung
1.d) Überstrapazierung der Resourcen (Zeit, Speicher, ...)
1.e) Nichtbearbeitung/Abfangen unerwarteter bzw. unmöglicher(!)
Eingaben.
1.f) Keine Maßnahmen, Fehlerausbreitung zu minimieren bzw. beim
Auftreten von Fehlern kontrolliert zu reagieren
1.g) Fehler in verwendeter, externer Software werden nicht in
Betracht gezogen (zB. Fehler in Compiler, Assembler, Linker, ...)
2) Hardwarefehler
1.a, 1.c, 1.f, wie oben
1.b wie oben (Betriebsspannung, machanische Belastung, Temperatur...)
1.g, 1.h wie oben für externe Komponenten
(Netzteile, Triebwerke, ...) und interne Komponenten wie
µC-Errata, Billigbauteile, die die Spezifikationen nicht
halten, ...
3) Bedienfehler
3.a Nichtbeachtung von Sicherheitsvorschriften, Ausserkraftsetzung von
Sicherheitsmechanismen aus Kosten-, Effizient- oder Bequemlichkeits-
Gründen
3.b Missverständliche Bedienungsanleitungen
3.c Schlecht geschultes oder überarbeitetes Bedienpersonal,
Fehleinschätzungen/Nichterkennung von Problem- und -gefahrenlagen
3.d Mangelne Redundanzplanung bei Modulausfällen
4) Systemische Fehler
Einzelkomponenten funktionieren und sind abgenommen, aber das
Zusammenspiel führt zu Fehlern
5) Physikalische "Fehler"
durch Rauschen, Einstreuungen, natürliche Radioaktivität,
Unschärfe, ...
Daher zB Test auf unmögliche Eingaben wie in 1.e.
6) Angriffe von Aussen
6.a Mangelnde Sicherheitseinrichtungen (Security)
Jungs, die Chipkarten knacken, spielen da zB auf hohem Niveau ;-)
und da muss man einiges beachten und einbauen um absichtliche
Systemkompromitierung zu erkennen/unterbinden (Temperatur, Spannung,
Laser, Elektronenstrahl, ...)
Teilweise ist der Quellcode in Hochsprache eher uninteressant. Analysen
wie WCET (worst code execution time) geschehen zB per abstrakter Analyse
auf Ebene der Maschinensprache. Verhalten von Pipelines und Cache,
Waitstates etc. müssen genau berücksichtigt und berechnet werden. Die
Ausführungsdauer von Code kann zB nach Verschieben von wenigen Bytes ein
komplett anderes Verhalten zeigen.
Je nach Gemengelage sind Compiler-Optimierungen nicht erlaubt, es sind
spezielle Sprachen und Code-Conventions vorgeschrieben, hinreichende
Testabdeckung, langjähriger Praxiseinsatz usw.
Neulich hatte ich die Gelegenheit, mit ein paar Jungs zu plaudern, die
Software für französische AKW zu zertifizieren haben. Ich möchte so ne
Arbeit echt nicht machen, allein bei dem Gedanken wird mit mulmig, für
wieviel Kilometer an auscompiliertem Spaghetticode die Korrektheit
zeigen müssen...
Johann
Auch wenns leicht off-topic ist würde mich interessieren, warum gerade Rekursion in Flugzeugen scheinbar/angeblich verboten ist? Jede rekursive Implementation ist leichter zu beweisen als eine Schleifenimplementation des gleichen "Algorithmus". Dies trifft insbesondere auf den Abbruch zu. Klar, Stacküberläufe treten um einiges schneller auf(wenn man nicht aufpasst)
> warum gerade Rekursion in Flugzeugen scheinbar/angeblich verboten ist
Na, wie viel Stack brauchst du denn ? Wenn du dir Rekursion nicht in (10
sich nacheinander aufrufende Funktionen) aufteilen kannst, weisst du das
offenbar nicht. So was fliegt nicht.
Es sind auch keine mallocs erlaubt, denn das, was man nicht vorher
vorhersehen kann und bytegenau angezaehlt hat, ist sowieso
fluguntauglich.
Kommt immer darauf an, wie sicherheitskritisch die Software ist. Was Software für das In-Flight-Entertainment betrifft, da ist so ziemlich alles erlaubt, wozu du Lust hast. Wenn es allerdings um Software im Autopiloten oder - noch schlimmer - in der Flugsteuerung geht, da wird schon sehr genau hingeschaut. Im Moment gibt es im wesentlichen nur ein einziges, ziemlich veraltetes Dokument, das schon erwähnte RTCA DO-178 B, "Software considerations in airborne equipment". Dieses stellt für die Zulassungsbehörden die Basis für weitere Verhandlungen dar. Hier werden zunächst einmal 5 sogenannte Software-Levels definiert, sortiert nach der Schwere der Folgen bei einem Bug. Ein Fehler in Level-"A"-Software hätte katastrophale Folgen (Flugzeug nicht mehr kontrollierbar), ein Fehler in Level "E" dagegen keinerlei sicherheitsrelevante Folgen. Ein Zulassungsprozess beginnt damit festzustellen, in welches Level die zu schreibende Software gehört. Stellt man fest, daß die Software zum Level "E" gehört, ist der Zulassungsprozeß schon beendet. Für alle höheren Levels definiert DO-178 B im wesentlichen einen Qualitätsmanagement-Prozeß und die einzelnen Schritte, die den kompletten Lebenszyklus der Software - von der Erstellung eines Anforderungskatalogs, der eigentlichen Implementierung, dem Test und schließlich der Konfiguration für die Laufzeit - umfassen. Eine wichtige Feststellung ist dabei, daß sämtliche Werkzeuge (Assembler, Compiler, Debugger, Test-Suiten) für den gleichen Software-Level zertifiziert sein müssen wie die zu erstellende Software selbst. Ausführlich beschrieben wird die korrekte Dokumentation der einzelnen Schritte des Lebenszyklus. Konkrete Forderungen für die Implementation gibt es eigentlich nicht. Das ist alles Verhandlungssache zwischen dem Hersteller und der Zulassungsbehörde. Es gibt objektorientierte Software, die nach DO-178 zertifiziert wurde - also scheint ein malloc() kein prinzipielles Problem darzustellen. Allerdings wird es wesentlich leichter, die Qualität einer Software zu bewerten und zu prüfen, wenn man auf Hochsprachen, dynamische Speicherverwaltung, Schleifen mit erst zur Laufzeit bekannter Zahl von Durchläufen und andere schwer zu "beweisende" Konstrukte verzichtet.
Thread beobachten
Seitenaufteilung abschaltenBitte melde dich an um einen Beitrag zu schreiben. Anmeldung ist kostenlos und dauert nur eine Minute.
Bestehender Account
Schon ein Account bei Google/GoogleMail? Keine Anmeldung erforderlich!
Mit Google-Account einloggen
Mit Google-Account einloggen
Noch kein Account? Hier anmelden.