» weiter" />

RSS Feeds – IMC OnAir, India meets Classic…

news feed aggregation for Indian (Music) Culture, Music therapy, Music pedagogy, Radio/TV

Software ist formal beweisbar

Diese Woche vermeldete Heise eine kryptische Botschaft: Microkernel seL4 ist beweisbar, fehlerfrei und unter Open Source gestellt. Für Einige ist das wohl eine nichtssagende oder völlig unverständliche  Nachricht – für Menschen aber, die sich mit Betriebssystemen und deren kleinen Macken beschäftigen, ist es ein Grund zur Freude.

Bei einem Kernel handelt es sich um das zentrale Element eines Betriebssystems – auf ihm bauen sozusagen alle weiteren Softwarebestandteile auf. Der Beweis, dass der Kern fehlerfrei ist, ist demnach eine kleine Sensation: “Alle Spezifikationen sind vollständig erfüllt”, heißt es.

Warum das wiederum so außergewöhnlich ist, darüber sprechen wir mit dem Hacker und IT-Experten Andreas Bogk, der uns erklärt, wie das korrekte Funktionieren eines Betriebssystems mathematisch bewiesen werden kann und was dies für Auswirkungen hat.

Foto: “ATC” von Sarah, CC BY-SA.20

 

 

Tagged as: , , , , , ,