Elektronik, diesmal gusseisern

Oh wei. Habe ich jetzt einen Patzer gemacht? Wie schreibt man das denn richtig?

Dieter Wiedmann schrieb:

Feinstofffeature?

--=20 mfg hdw

Alleine die Tatsache, dass es mehr als eine Release des Compilers gibt (aktuell scheint 7.5 zu sein) beweist schon, dass zumindest fuer den Compiler kein Korrektheitsbeweis gefuehrt wurde. Damit gilt das auch fuer alle Compilate.

Aber selbst wenn es einen korrekten Compiler gaebe, schuetzt das nicht vor Fehlern im Code die zu Ausgaben fuehren die zwar im spezifizierten Bereich liegen, aber zum falschen Zeitpunkt erfolgen.

Du kannst recht nahe rankommen, aber einen vollstaendigen Beweis der Korrektheit einer Implementation incl. Hardware wirst du nicht fuehren koennen.

Gerrit

Richtig heißt es: Damit _Linux_ .... absturzfrei .... wird viel neu geschrieben und kompiliert ....

Du hast Vorurteil #1 versehentlich auf Windows angewandt ;-)

Falk

Wir haben hier einen Ingenieur, der eigentlich SPS-Programmierung macht, der kommt auf solche Ideen, während des Wechsels zwischen zwei Bildschirmen auf die Help-Taste zu drücken und damit das Gerät zu killen. Er heißt auch Jörg - Zufall? Jedenfalls, wenn unser Gerät mit einer neuen Softwareversion fehlerfrei eine Integration in eine Anlage durch Jörg überlebt hat, dann kann man es auf die Kunden loslassen.

Dann gibt es noch den Uwe-Test - Uwe war mal ein Praktikant, der es drauf hatte, auf dem Touchscreen irgendwo mitten drin reinzutatschen und das Gerät damit zu töten. Macht halt auch kein normaler Mensch, irgendwo hindrücken, wo es gar kein Eingabefeld gibt. War uns eine Lehre :)

Uwe emulieren wir mit vereinten Kräften, Jörg wird darauf losgelassen...dann ist schon mal ein erster Härtetest bestanden.

Eh klar; unser Kram hat keinen Button "shutdown", zum Abschalten wird einfach über den Schlüsselschalter hart der Strom abgeschaltet, und außer bei gerade laufenden firmwareupgrades ist das in jedem Falle erlaubt. Bei besagten upgrades passiert übrigens auch nix, außer, daß halt wieder auf die alte Version zurückgeschaltet wird. Wir haben einen Speicherbereich, der nur im Werk beschrieben wird, also ist immer der schmerzfreie Rückweg zur Auslieferversion drin.

Ralph.

Hmm, hier was um 30 kbyte/sec :( Falls es durchläuft, kann ich es gerne besser angebunden ablegen, link gibts bei Bedarf per email.

Ralph.

Wieso sollte ein neues Release beweisen, daß kein Korrektheitsbeweis für den Compiler existiert?

Das wäre für mich dann aber ein gravierender Fehler in der Spezifikation. Reaktionszeiten werden ja schon für normale Businessprogramme definiert, und das noch nicht mal allzu formal, z.B. "wenn der User auf 'Formular abschicken' klickt, dann darf die Wartezeit für den User maximal 1 Sekunde betragen, bis er Daten in ein neues Formluar eintragen kann".

Die Release Note enthaelt das Wort 'Corrections'. Man koennte da auch 'Bug fix' schreiben.

In der Spezifikation kann es ja drinstehen. Bleibt die Frage, wie du beweist, dass sich das Compilat unter allen Umstaenden an die Spec haelt.

Alles was ich finden konnte redet immer nur von 'high integrity'. Wird schon einen Grund haben warum da 'high' und nicht 'full' steht.

Gerrit

In article , Frank Buss writes: |> |> Wieso sollte ein neues Release beweisen, daß kein Korrektheitsbeweis für |> den Compiler existiert?

Ich frag mal andersrum: Hast Du Dir mal den Zustandsautomaten des Nim-Spiels angeschaut? Muß gar nicht weit sein, sagen wir bis zur vierten Reihe. Da fischt Du nun alle Zustände raus, die Dich zum Sieg führen, egal wie sich Dein Kontrahent verhält (ja, das geht).

Nun ist das Nim-Spiel etwas formal spezifiziertes mit *sehr* einfachen Regeln und extrem einfachen Ein-/Ausgaben.

Und dennoch explodiert der Zustandsautomat.

Jetzt kommst Du und machst es nicht nur mit dem Compiler sondern auch mir dem Compilat... Da frage ich mich direkt, warum Du noch nicht mit dem Turing-Award ausgezeichnet wurdest und *den* Lehrstuhl für theoretische Informatik innehast.

Rainer

Erledigt. Bei Interesse bitte email.

Ralph.

Ralph A. Schmid, dk5ras schrieb:

Von der Vorstellung sollte man sich schleunigst lösen, bevor man Testfälle konstruiert - sowohl bei Hardware, als auch bei Software.

BTW: Die Abstufung robust, unkaputtbar, BOS-tauglich müsstest du auch noch aus deinem vorherigen Job kennen, oder? ;-)

Gruß Bernd

'Correction' könnte auch sein, daß der Compiler mit einer Fehlermeldung abbricht, wenn man Identifier länger als 32 Zeichen verwendet und das man jetzt beliebig lange Identifier verwenden kann. Müsste man sich mal genauer ansehen, hast du einen Link?

Wenn sowas wie Netzwerkkommunikation, Internet usw. mit drin ist, dann wird das wohl nicht gehen. Wenn es darum geht, eine maximale Antwortzeit per serieller Schnittstelle von einem Messsystem festzulegen, dann sollte das unter allen Umständen möglich sein. Gibt ja schließlich auch sowas wie hartes Realtime Systeme, die auch eine garantierte Antwortzeit bieten.

Bei Software immer davon ausgehen, dass alle Eingangsdaten boese sind bis du das Gegenteil bewiesen hast und alles bis auf die in diesem Zustand erlaubten Werte ausmaskiert hast.

Gerrit

Ich brauche mir für einen Beweis ja nicht alle Zustände anzusehen, sondern nur nachzuweisen, daß der Zustandsautomat die Spezifikation implementiert. Wenn die Spezifikation natürlich verlangt, bei einem Schachspiel oder was auch immer, garantiert zu gewinnen oder ein ELO von > 2000 zu erreichen, dann wird es schwierig :-)

Ja, frage ich mich manchmal auch :-) Für einen Compiler die Korrektheit nachzuweisen könnte aber schon schwieriger sein.

Auch das von dir beschriebene waere ein Bug und duerfte bei einem vollstaendig auf Korrektheit geprueften Compiler nicht passieren.

Och, schon IRQs koennen fuer interessante Probleme sorgen weil sie eben auch Zeit brauchen und damit das Timing verbiegen koennen. Sowas zu debuggen macht Spass wenn man eine Race-Condition drin hat die nur dann getriggert wird wenn der IRQ in einem bestimmten Code-Stueck passiert.

Mehr als eine IRQ-Quelle und die Sache wird noch spassiger.

Gerrit

Das kannst du auf virtueller Hardware machen, aber auf realer Hardware musst du erstmal nachweisen, dass dein Zustandsautomat auch wirklich nur die in der Spec vorgeschriebenen Uebergaenge hat oder ob sich, aufgrund von Fehlern in der Hardware (*), noch andere Uebergaenge ergeben koennen. Man stelle sich vor, dass wenn im Register X der Wert Y steht auf einmal auch Bit 7 aus Register Z den Uebergang beeinflusst. Wenn Null, dann nach Zustand A und wenn 1 nach Zustand B. Kommt eher selten vor, aber fuer einen Korrektheitsbeweis musst du alles durchprobieren. Das kann bei einer entsprechenden Menge an Registern eine Weile dauern. Vielleicht reicht es bis zum naechsten Big Bang...

(*) Die natuerlich nicht alle im Datenblatt beschrieben sind. Aber wer kennt diese Probleme nicht?

Zum Thema Verifikation von Hardware... Ich hatte hier 2 Speichermodule die jeden Softwarebasierten Speichertest bestanden haben den ich finden konnte. Trotzdem ist die Kiste mit diesen Modulen immer abgeschmiert. Umgetauscht (gleicher Hersteller und Fabrikat) und alles geht. OK, in Systemen mit hoher Zuverlaessigkeit wird ECC-Speicher, u.U. noch mit Spiegelung verwendet (hoffe ich zumindest!). Da bleibt dann die Frage nach der Zuverlaessigkeit der ECC-Logik

Man kann bis zu einem bestimmten Level testen und verifizieren (**). Aber ab einem bestimmten Punkt muss man bei nicht-trivialer Software auf nicht-trivialer Hardware einfach hoffen nichts uebersehen zu haben.

(**) Dieser Level ist natuerlich abhaengig von der Zahlungswilligkeit des Kunden und laesst einen breiten Spielraum zu, beginnend von 'it compiles, ship it'.

Gerrit

Hardwarefehler kann man generell nicht durch Tests ausschließen. Bei sicherheitskritischen Systemen wird das daher mehrfach aufgebaut, z.B. dreimal, und ein Ergebnis nur dann als gültig anerkannt, wenn es mehr als ein System geliefert hat. Klar, kann dann immer noch bei der Abstimmungslogik Fehler geben, aber die ist relativ einfach im Vergleich zu einem Prozessor. Wenn man es dann noch von unterschiedlichen Teams und mit unterschiedlichen Computersprachen und Computersystemen implementiert, dann sollten sowohl Hardwarefehler, als auch Softwarefehler recht unwahrscheinlich werden.

Das geht aber nur, wenn das dann auch 3 verschiedene CPUs sind, sonst kannst du einem bisher unentdeckten Bug aufsitzen und deine Dreifachauslegung hilft nicht weil alle drei CPUs dasselbe, aber falsche Ergebnis liefern. :)

Gerrit

Ja, das meinte ich mit "unterschiedliche Computersysteme". Am besten drei Black-Boxes, wo nur digitale Signale parallel rein gehen und Steuersignale raus kommen, die dann verglichen werden. Sowas werden aber wohl die wenigsten Auftraggeber bezahlen.