1. Foren
  2. Kommentare
  3. Wissenschaft
  4. Alle Kommentare zum Artikel
  5. › Sel4: Fehlerloser Microkernel…

WAT?

  1. Thema

Neues Thema Ansicht wechseln


  1. WAT?

    Autor: majablagdan 29.07.14 - 12:37

    Satz von Rice? Halteproblem? Worst Case Execution Time? Alle Probleme gelöst! K. Gödel wäre begeistert.

  2. Re: WAT?

    Autor: Nephtys 29.07.14 - 12:51

    majablagdan schrieb:
    --------------------------------------------------------------------------------
    > Satz von Rice? Halteproblem? Worst Case Execution Time? Alle Probleme
    > gelöst! K. Gödel wäre begeistert.

    Fast sinnvoller Post. Warum ist er das trotzdem nicht?

    Eine Endlosschleife des Betriebssystems schützt sich selbst. Dein OS mag dadurch abschmieren, aber es gibt keine Möglichkeit diese Lücke auszunützen, um zB an Daten zu kommen. Darum geht es hier.
    Deshalb muss nur getestet werden, ob für alle endlichen Berechnungen Lücken entstehen. Und das kann man bei einem solchen Microkernel doch recht gut.

    Von daher hat es NICHTS mit dem Halteproblem zu tun.

  3. Re: WAT?

    Autor: ai114 29.07.14 - 13:02

    http://ertos.nicta.com.au/research/l4.verified/

    Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel: Isabelle/HOL A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, Vol. 2283, 2002

    Lesen bildet.

    Gruss
    gwe

  4. Re: WAT?

    Autor: lestard 29.07.14 - 13:39

    Beim Satz von Rice und dem Halteproblem geht es ja darum Eigenschaften über beliebige Algorithmen allgemein zu entscheiden (vereinfacht gesagt). Gibt es ein Programm, dass für einen beliebigen Algorthmus entscheidet, ob er anhält oder nicht?

    Für bestimmte Arten/Klassen von Algorithmen kann man aber sehr wohl solche "Entscheider" entwickeln. So ein Micro-Kernel z.B. hat ja nur einen begrenzten Satz an Aufgaben.

  5. Re: WAT?

    Autor: frostbitten king 29.07.14 - 15:15

    Mjain. War nicht grad talentiert beim Complexity Theory Teil der Formalen Methoden der Informatik Vorlesung, aber ein Teil (Software Verification), hat sich mit der Thematik wie du Software Formal auf Fehlerfreiheit überprüfen kannst beschäftigt.
    [de.wikipedia.org]. Mit dem Hoare Kalkül kannst du dann trotzdem Schleifen auf Total Correctness überprüfen: Jetzt frei aus dem Gedächtnis, wenn ein Loopbody p die Precondition erfüllt (sprich der Loopbody wird ausgeführt), dann terminiert die Loop(nach Erfüllung der Terminationsbedingung), und das Ergebnis ist korrekt (mit dem Total Correctness Proof lässt sich die Frage, _ob_ eine Schleife terminiert beantworten -> natürlich auch was sie zürckliefern soll lt. Spec)..
    Ich vermute die haben ua. den/das (gah) Hoare Kalkül dafür verwendet.

  6. Re: WAT?

    Autor: dit 29.07.14 - 16:09

    majablagdan schrieb:
    --------------------------------------------------------------------------------
    > Satz von Rice? Halteproblem? Worst Case Execution Time? Alle Probleme
    > gelöst! K. Gödel wäre begeistert.

    immer hin du hast es versucht.

  7. Re: WAT?

    Autor: 486dx4-160 29.07.14 - 18:14

    Kannst du dich mal festlegen auf Deutsch oder Englisch festlegen? Dieser Mischmasch ist unglaublich schlecht zu lesen.

  8. Re: WAT?

    Autor: Hello_World 30.07.14 - 00:01

    Das Halteproblem sagt aus, dass es keinen Algorithmus gibt, der für jedes beliebige Programm entscheidet, ob es hält oder nicht. Und das heißt eben *nicht*, dass man es für ein konkretes nicht doch zeigen könnte. Analoges gilt für den Satz von Rice.

    Aber na ja, ist man ja mittlerweile gewöhnt, dass bei jedem derartigen Thema irgendjemand mit Sätzen um sich wirft, die er nicht verstanden hat.

  9. Re: WAT?

    Autor: frostbitten king 30.07.14 - 14:11

    Ok, ja das ist wohl wahr der Mischmasch ist in der Tat grauslich (ich kotz bei so nem Mischmasch wenn das wer Anderer schreibt auch ab), Asche auf mein Haupt.
    ..
    Werde das mal versuchen zu minimieren...Argh.. man kann ja nach 5min nicht mehr seine Beiträge korrigieren.
    --------------------------------------------------------------------------------
    > Mjain. War nicht grad talentiert beim Komplexitätstheorie Teil der Formalen
    > Methoden der Informatik Vorlesung, aber ein Teil (Software Verifikation),
    > hat sich mit der Thematik wie du Software formal auf Fehlerfreiheit
    > überprüfen kannst beschäftigt.
    > [de.wikipedia.org]. Mit dem Hoare Kalkül kannst du dann trotzdem Schleifen
    > auf Totale Korrektheit überprüfen: Jetzt frei aus dem Gedächtnis, wenn ein
    > (ka. wie ma das auf Deutsch kompakt nennt) zu wiederholender Teil p die Vorbedingung erfüllt (sprich der Schleifenkörper? wird ausgeführt),
    > dann terminiert die Schleife(nach Erfüllung der Terminationsbedingung), und das
    > Ergebnis ist korrekt (mit dem Totalen Korrektheitsbeweis lässt sich die Frage,
    > _ob_ eine Schleife terminiert beantworten -> natürlich auch was sie
    > zürckliefern soll lt. Spec)..
    > Ich vermute die haben ua. den/das (gah) Hoare Kalkül dafür verwendet.
    Besser?



    4 mal bearbeitet, zuletzt am 30.07.14 14:23 durch frostbitten king.

  1. Thema

Neues Thema Ansicht wechseln


Um zu kommentieren, loggen Sie sich bitte ein oder registrieren Sie sich. Sie müssen ausserdem in Ihrem Account-Profil unter Forum einen Nutzernamen vergeben haben. Zum Login

Stellenmarkt
  1. IT-Architektin (m/w/d)
    Techniker Krankenkasse, Hamburg
  2. IT Systemadministrator (m/w/d)
    Franz Mensch GmbH, Buchloe
  3. IT-Systemadministrator*in (m/w/d)
    Universität Osnabrück, Osnabrück
  4. IT Senior Softwareentwickler (m/w/d)
    CG Car-Garantie Versicherungs-AG, Freiburg im Breisgau

Detailsuche


Golem pur
  • Golem.de ohne Werbung nutzen

Anzeige
Hardware-Angebote
  1. 499,99€


Haben wir etwas übersehen?

E-Mail an news@golem.de