Die Firma für die ich im letzten Jahrtausend gearbeitet habe, hat seinerzeit das Kabinenkommuniationssystem für Airbus entwickelt, mit der Methode der formalen Verifikation. Da kann man dann mathematisch beweisen, dass der Code genau das tut, was spezifiziert wurde.
Formale Verifikation machen wir auch bis runter zu DAL E, was nicht den mathematischen Beweis erfordert, sondern "nur" die überprüfbare Abdeckung und das Tracing aller Anforderungen (Spezifikation). Mathematische Beweise sind nur für DAL A und B vorgeschrieben.
Und das Kabinenkommunikationssystem soll DAL A oder B sein? Hm...?
Oder habt ihr das einfach so mathematisch bewiesen, weil ihr das Ganze ohnehin in MathLab designt habt? ![]()