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

WAT?

Neue Foren im Freiraum! Raumfahrt und freie Software haben jetzt einen Platz, die Games tummeln sich jetzt alle in einem Forum.
  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-Systemtechniker in der Leit- und Kommunikationstechnik der Werkfeuerwehr (m/w/d)
    CURRENTA GmbH & Co. OHG, Leverkusen, Dormagen, Krefeld-Uerdingen
  2. Data Warehouse Betreuer (w/m/d)
    Investitionsbank Schleswig-Holstein, Kiel
  3. Datenbank-Administrator (m/w/d)
    KVJS - Kommunalverband für Jugend und Soziales Baden-Württemberg, Stuttgart
  4. Frontend Technology Consultant (m/w/d)
    Haufe Group, Sankt Gallen (Schweiz) (Home-Office möglich)

Detailsuche


Golem pur
  • Golem.de ohne Werbung nutzen

Anzeige
Spiele-Angebote
  1. 49,99€
  2. 1,99€
  3. 32,99€
  4. 14,49€


Haben wir etwas übersehen?

E-Mail an news@golem.de


Roku Express im Test: Die Fire-TV-Konkurrenz hat ein paar Schwächen zu viel
Roku Express im Test
Die Fire-TV-Konkurrenz hat ein paar Schwächen zu viel

Die ersten Roku-Geräte für den deutschen Markt sind vor allem eine Konkurrenz zum Fire TV Stick. Die Neulinge bieten Besonderheiten - nicht nur positive.
Von Ingo Pakalski

  1. Roku Streambar Soundbar mit Streamingfunktionen kostet 150 Euro
  2. Konkurrenz zu Fire-TV-Sticks Roku bringt Streaming-Gerät für 30 Euro
  3. Roku TV-Stick mit angepasstem Linux kommt nach Deutschland

Bosch Nyon im Test: Die dunkle Seite des Tachos
Bosch Nyon im Test
Die dunkle Seite des Tachos

Connected Biking nennt Bosch seine Lösung für aktuelle Pedelecs - wir sind mit dem Fahrradcomputer Nyon geradelt und nicht vom Weg abgekommen.
Ein Test von Martin Wolf

  1. Electrom Liege-E-Bike mit Allrad und Stromlinien-Hülle
  2. VanMoof V Vanmoof kündigt S-Pedelec an
  3. Tiler E-Bikes kabellos über den Fahrradständer laden

Astrofotografie: Der Himmel so nah
Astrofotografie
Der Himmel so nah

Wer den Nachthimmel fotografiert, erfasst viel mehr als mit bloßem Auge. Wir geben Tipps für den Einstieg in das faszinierende Hobby Astrofotografie.
Eine Anleitung von Mario Keller