mikrocontroller.net

Forum: Compiler & IDEs Korrektheit beweisen


Autor: Gerhard (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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

???

Autor: Mark Brandis (markbrandis)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
Es ist nicht möglich zu beweisen, dass ein Algorithmus terminiert. 
("Halteproblem")

Autor: Karl Heinz (kbuchegg) (Moderator)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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.

Autor: Mark Brandis (markbrandis)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
...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.

Autor: Oliver Döring (odbs)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
Gib mir ein Schnipsel Assembler, und ich sage dir, ob er für alle 
Eingabewerte terminiert. "Beweis durch Hinschauen".

Autor: Mark Brandis (markbrandis)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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?

Autor: Oliver Döring (odbs)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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.

Autor: MaWin (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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.

Autor: Rolf Magnus (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
> 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.

Autor: MeinerEiner (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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.

Autor: Oliver Döring (odbs)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
> 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.

Autor: Oliver Döring (odbs)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
> 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 ;)

Autor: Klaus Falser (kfalser)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
Diese Redundanzen ergeben aber keinen Beweis der Korrektheit, sondern 
verringern nur die Fehlerwahrscheinlichkeit.

Das ist ein kleiner, aber feiner Unterschied!

Autor: Oliver Döring (odbs)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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.

Autor: Johann L. (gjlayde) Benutzerseite
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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

Autor: Matthias Larisch (matze88)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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)

Autor: MaWin (Gast)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
> 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.

Autor: Oliver Döring (odbs)
Datum:

Bewertung
0 lesenswert
nicht lesenswert
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.

Antwort schreiben

Die Angabe einer E-Mail-Adresse ist freiwillig. Wenn Sie automatisch per E-Mail über Antworten auf Ihren Beitrag informiert werden möchten, melden Sie sich bitte an.

Wichtige Regeln - erst lesen, dann posten!

  • Groß- und Kleinschreibung verwenden
  • Längeren Sourcecode nicht im Text einfügen, sondern als Dateianhang

Formatierung (mehr Informationen...)

  • [c]C-Code[/c]
  • [avrasm]AVR-Assembler-Code[/avrasm]
  • [code]Code in anderen Sprachen, ASCII-Zeichnungen[/code]
  • [math]Formel in LaTeX-Syntax[/math]
  • [[Titel]] - Link zu Artikel
  • Verweis auf anderen Beitrag einfügen: Rechtsklick auf Beitragstitel,
    "Adresse kopieren", und in den Text einfügen




Bild automatisch verkleinern, falls nötig
Bitte das JPG-Format nur für Fotos und Scans verwenden!
Zeichnungen und Screenshots im PNG- oder
GIF-Format hochladen. Siehe Bildformate.
Hinweis: der ursprüngliche Beitrag ist mehr als 6 Monate alt.
Bitte hier nur auf die ursprüngliche Frage antworten,
für neue Fragen einen neuen Beitrag erstellen.

Mit dem Abschicken bestätigst du, die Nutzungsbedingungen anzuerkennen.