@Simon.F
Zu deiner PN, ich hatte ja geschrieben daß ich dir lieber hier antworte, weil das einer erschöpfenden Diskussion dienlicher ist:
Vorweg, ich arbeite auch nicht mit Verifizierungstools. Was ich dir dennoch sagen kann:
-Software für Anwendungen wie Automotive oder gar Luft- und Raumfahrt oder Medizintechnik zu zertifizieren, ist ein irrer Aufwand. Software, die andere Software für solche Anwendungen zertifiziert, ist noch weitaus aufwendiger. Sofern ich mal mit zertifizierter Software gearbeitet habe, wirkten diese Programme immer so als war das die erste Betaversion: völlig vermurkste Oberfläche, unverständliche Bezeichnungen, unlogisch in der Bedienung, teils offen fehlerhaft (Klick auf Button macht was völlig unerwartetes), Hilfsautomatismen die mehr Arbeit machen alsdaß sie helfen. Teamcenter Cockpit (Versionierung für Luftfahrt) ist da so ein Beispiel.
Der Grund dafür ist der verflucht aufwendige Zertifizierungsprozess: Ist da ein Release einmal durch, fasst man das nach Möglichkeit nicht an wenn es nicht unbedingt sein muß. Da rollt man nicht einfach mal so ein Update aus um irgendwelche Kleinigkeiten zu verbessern, oder die GUI umzustricken.
Mit Programmen, deren Ausgabe die Grundlage für Zertifizierungen sind, ist das garantiert nicht besser.
Selbst wenn du ein Programm hast, schätze ich mal daß der Markteintritt sehr schwierig wird. Wenn du so ein Programm z.B. für Luftfahrtprozesse verkaufen willst, müßtest du wahrscheinlich Boeing und/oder Airbus davon überzeugen, Lieferanten zu akzeptieren die dein Programm verwenden. Für die OEMs und deren Lieferanten wäre es erstmal ein Vorteil, wenn es in der Lieferkette etwas mehr Wettbewerb gibt.
Allerdings kann es dann aber leicht passieren, daß du einer Firma wie Siemens, die bis dahin sehr viel Geld für wenig Arbeit (sieht man mal von der initialen Veröffentlichung ab) verdient haben, mit deiner Software vors Schienbein trittst. Dann findet irgendein Mittagessen zwischen hinreichend hohen Managern statt, dort wird deine Software besprochen, und danach wird niemand deine Software kaufen können weil es vom Kunden dafür keine Freigabe gibt obwohl alle vorher hellauf begeistert waren.
Noch ein paar Gedanken zum Thema an sich:
Sehr viel, wenn nicht die meiste, Software für wichtige Dinge wird ja heute in C geschrieben. Wichtig heißt, es hängt sehr viel Geld oder Menschenleben von der Funtion der Software ab.
Für C gibt es aber meines Wissens nach bereits jede Menge (oder zumindest ausreichend) Analysetools für solche Zwecke. Und auf solchen Märkten mitzuspielen wird nicht einfach.
Jetzt kommt noch dazu: C ist für solche Anwendungen nie gemacht worden. Ich nannte C ja eine altehrwürdige Krüppelsprache bezeichnet - tatsächlich ist C ja uralt. Sechzig Jahre? Siebzig Jahre? Seitdem hat sich viel getan in der Softwareentwicklung, viele Lektionen wurden gelernt und denen wird C einfach nicht mehr gerecht, und die statischen Codeanalysetools können eigentlich auch nicht mehr als den Funktionsumfang von C zu beschränken und Dinge wie Pointerarythmetik oder bool aus Zahlen abzuleiten zu verhindern.
Altehrwürdig, weil C uns schon weit gebracht hat – aber ich finde, man sollte es heute wirklich in Rente schicken. Für wichtige Dinge (viel Geld, Menschenleben) wurde ja z.B. mal Ada gemacht, aber es ist schwierig, dafür Programmierer zu finden, C kennt dagegen jeder.
Was ich mir wünschen würde wäre eine neue Programmiersprache, die darauf optimiert ist inhärent sicher zu sein was gängige Sicherheitsrisiken wie Überläufe oder dergleichen ausschließt.
Rust z.B. schickt sich ja gerade an, das Steckenpferd von C – hardwarenahe Programmierung – zu übernehmen. Ich habe mich mit Rust noch nicht befasst (kommt aber noch), aber es wäre interessant zu wissen ob und wie solche Fehlervermeidung/Verifikationsmöglichkeiten in Rust bereits eingebaut sind. Oder noch eingebaut werden könnten.
Das würde einen möglichen Markteintritt auch vereinfachen: Sei dem schnarchenden Konzern einfach weit genug vorraus, biete Werkzeuge an die in geringem Umfang kostenlos genutzt werden können (nichtzertifizierte Communityversion oder dergleichen), und lasse dich von Siemens, irgendeinem Autokonzern, Pharmatechnikkonzern, Thales, ... für teuer Geld aufkaufen.
Edit:
Vielleicht noch ganz lehrreich:
An interactive learning platform to teach the Ada and SPARK programming languages.
learn.adacore.com
Damit du siehst wie eine Programmiersprache für kritische Anwendungen funktioniert.
