Was macht Ada zur Sprache der Wahl für die sicherheitskritischen Systeme der ISS?

Dieser Wikibooks-Link listet seine Stärken auf, von denen einige sind:

• Ein extrem starkes, statisches und sicheres Typsystem, das es dem Programmierer ermöglicht, leistungsstarke Abstraktionen zu konstruieren, die die reale Welt widerspiegeln, und dem Compiler ermöglicht, viele logische Fehler zu erkennen, bevor sie zu Fehlern werden.
• Modularität, wobei der Compiler direkt die Konstruktion sehr großer Softwaresysteme aus Quellen verwaltet.
• Ausblenden von Informationen; Die Sprache trennt Schnittstellen von der Implementierung und bietet eine feinkörnige Kontrolle über die Sichtbarkeit.
• Lesbarkeit, die Programmierern hilft, Code zu überprüfen und zu verifizieren. Ada bevorzugt den Leser des Programms gegenüber dem Schreiber, denn ein Programm wird einmal geschrieben, aber viele Male gelesen. Zum Beispiel verbietet die Syntax alle mehrdeutigen Konstrukte, so dass es keine Überraschungen gibt, in Übereinstimmung mit dem Gesetz des geringsten Erstaunens des Tao der Programmierung. (Einige Ada-Programmierer sprechen nur ungern über Quellcode, der oft kryptisch ist; sie bevorzugen Programmtext, der englischer Prosa nahe kommt.)
• Portabilität: Die Sprachdefinition erlaubt es Compilern, sich nur auf wenige kontrollierte Arten zu unterscheiden, und definiert ansonsten die Semantik von Programmen sehr genau; Infolgedessen ist der Ada-Quelltext über Compiler und Zielhardwareplattformen hinweg sehr portabel. Meistens kann das Programm ohne Änderungen neu kompiliert werden.
• Standardisierung: Standards sind seit der Gestaltung der Sprache in den späten 1970er Jahren ein Ziel und ein herausragendes Merkmal. Der erste Standard wurde 1980 veröffentlicht, nur 3 Jahre nach Beginn des Designs. Ada-Compiler unterstützen alle genau dieselbe Sprache; der einzige Dialekt, SPARK, ist lediglich eine annotierte Teilmenge und kann mit einem Ada-Compiler kompiliert werden.

Der Punkt der Lesbarkeit ist ein wichtiger Punkt, da die Lebensdauer eines Softwareprodukts nicht endet, wenn Sie es fertig programmiert/getestet haben. Der größte Aufwand (in Zeit und Geld) besteht in der Wartung dieses Produkts. Für ein langes Projekt wie die ISS erscheint es daher angemessen, eine Sprache zu verwenden, die entwickelt wurde, um bei dieser Aufgabe zu helfen, indem Fehler und allgemeine Mehrdeutigkeiten minimiert werden.

Diese Antwort vergleicht es mit C und C++:

Ada hat eine Reihe von Sicherheitsfunktionen in die Sprache integriert. (Vergleichen Sie mit C, wo der Standard zwölf Seiten hat, die die in die Sprache eingebauten undefinierten Verhaltensweisen zusammenfassen. Vergleichen Sie mit C++, wo die undefinierten Verhaltensweisen so zahlreich sind, dass sie sie nicht einmal auflisten.) Diese Ada-Sicherheitsfunktionen können von Bedeutung sein Leistungskosten, und aus diesem Grund bietet Ada auch die Möglichkeit, diese Sicherheitsfunktionen selektiv zu deaktivieren.

Beachten Sie, dass es möglich ist, das gleiche Sicherheitsniveau mit C oder C++ zu erreichen, wenn Sie eine Teilmenge der C- oder C++-Sprachen verwenden und sich auf einen Styleguide festlegen, aber in Ada kommt es mit der Sprache.

EDIT (Danke JCRM): Der erste Link spricht auch über die Unterstützung für Low-Level-Programmierung:

Ada verfügt über leistungsstarke Spezialfunktionen, die die Low-Level-Programmierung für Echtzeit-, sicherheitskritische und eingebettete Systeme unterstützen. Zu diesen Funktionen gehören unter anderem Maschinencode-Einfügungen, Adressarithmetik, Low-Level-Zugriff auf den Speicher, Kontrolle über die bitweise Darstellung von Daten, Bitmanipulationen und ein wohldefiniertes, statisch beweisbares Concurrent-Computing-Modell namens Ravenscar Profile.

Wo ich arbeite, verwenden wir tatsächlich die Adressarithmetik und die Low-Level-Memory-Funktionen, um verschiedene Konfigurationsdaten zu laden, ohne das Produkt jedes Mal neu kompilieren zu müssen, was viel Zeit spart.

Zeitliche Koordinierung. Ada wurde in den 1970er und 80er Jahren mit der Absicht entwickelt, die Fülle von Sprachen zu ersetzen, die in den Echtzeitsystemen des US-Verteidigungsministeriums verwendet werden. Die NASA (und auch Organisationen aus Europa) waren aktive Teilnehmer. Das Verteidigungsministerium beauftragte Ada 1991 mit allen wichtigen Entwicklungen. Die NASA tat das Gleiche. Die Internationale Raumstation war bis dahin ein Papierkonzept. Genau mit dem Inkrafttreten des Ada-Mandats begann es Realität zu werden.

Das Verteidigungsministerium ließ 1997 sein Ada-Mandat fallen. Die NASA tat dasselbe. Wenn die ISS heute gebaut würde, wäre ihre Flugsoftware höchstwahrscheinlich nicht in Ada.

Warum also Ada? Ada wurde geschaffen, um eine Reihe von Problemen anzugehen. Einer war die große Anzahl von Sprachen, die beim Verteidigungsministerium verwendet wurden. Ein weiterer Grund war der wahrgenommene Mangel an Sicherheit in diesen Sprachen, insbesondere in Bezug auf Echtzeitsysteme und eingebettete Systeme. Ada hat einige Funktionen bereitgestellt, die in anderen Sprachen fehlten.

Es gibt viele Gründe, warum Ada zu einer Nischensprache geworden ist. Einer davon ist, dass die übermäßige Strenge und Ausführlichkeit der Sprache einer Allzwecksprache im Weg stehen. Ein weiteres Problem war, dass die Ada-Community beim Übergang von Großrechnern zu Minicomputern zu Desktop-Computern den Anschluss verpasste. Die Sprachen an der Spitze dieser Übergänge (C und C++) bleiben weit verbreitet. Auch die Ada-Community hat den Anschluss an die Freie-Software-Bewegung verpasst. Der erste kostenlose Ada-Compiler kam erst 1995 heraus, und diese Veröffentlichung war noch nicht vollständig. Da war es zu spät.

Ich erinnere mich, dass ich Ende der 90er Jahre Informatikkurse besuchte. Der Professor für CS erklärte unserer mageren Gruppe von CS-Majors, dass er uns C beibringen würde und nicht COBOL oder Ada, weil es im Allgemeinen nützlicher wäre. Zu dieser Zeit waren sie die wichtigsten Programmiersprachen-Colleges, die damals unterrichtet wurden (jede größere Universität in der Region mit einem Informatik-Abschluss lehrte einen dieser beiden). Warum sollten sie ältere Sprachen unterrichten? Weil Sie immer noch einen Job bekommen könnten, der Code in ihnen schreibt. Das war ungefähr zu der Zeit, als die ISS gebaut wurde.

Der Grund, warum Ada entstand, war, dass sie geschäftskritische Software brauchten, die zuverlässig war, und Ada wurde buchstäblich dafür gemacht, die Rechnung zu erfüllen. Die NASA hat immer noch einen der teuersten Softwarefehler der Geschichte (zurück in die dunklen Zeiten der Lochkarten )

Ein durch eine Lochkarte eingeführter Fehler stellte sich als einer der teuersten Softwarefehler der Geschichte heraus, als er 1962 zur Zerstörung des Raumschiffs Mariner 1 führte (Kosten 1962: 18,5 Millionen Dollar; Kosten in heutigen Dollar: 135 Millionen Dollar). ), bevor es seine Mission erfüllen konnte, an der Venus vorbeizufliegen.

Allerdings gab es einen fatalen Fehler in der Software dieses Leitsystems: Als die Gleichungen, die zur Verarbeitung und Übersetzung von Tracking-Daten in Fluganweisungen verwendet wurden, auf Lochkarten kodiert wurden, wurde ein entscheidendes Symbol weggelassen: oft ein Überstrich oder Überstrich in den Folgejahren mit einem Bindestrich verwechselt. Das Fehlen dieses Überbalkens führte im Wesentlichen dazu, dass der Leitcomputer eine ansonsten normale Bewegung im Raumfahrzeug falsch kompensierte.

Adas Hauptmerkmal ist Stabilität

Mit seinem Schwerpunkt auf soliden Software-Engineering-Prinzipien unterstützt Ada die Entwicklung von Anwendungen mit hoher Integrität, einschließlich solcher, die nach Sicherheitsstandards wie DO-178B und Sicherheitsstandards wie den Common Criteria zertifiziert werden müssen. Starke Typisierung bedeutet beispielsweise, dass auf Daten, die für einen bestimmten Zweck bestimmt sind, nicht über unangemessene Vorgänge zugegriffen wird; Fehler wie das Behandeln von Zeigern als ganze Zahlen (oder umgekehrt) werden verhindert. Und die Überprüfung der Array-Grenzen von Ada verhindert Pufferüberlauf-Schwachstellen, die in C und C++ üblich sind.

Die NASA hat versucht, ihre eigene Ada-ähnliche Sprache namens (ich erfinde das nicht) HAL/S zu erstellen , die das Space Shuttle verwendet hat, und ... nicht viel mehr. Die gesamte Bodenausrüstung würde bis dahin mit Ada enden ( Standards! )

Ein Vorschlag für eine bodengestützte NASA-Standardversion von HAL mit dem Namen HAL/G für "Ground" wurde vorgeschlagen, aber das bevorstehende Auftauchen der bald Ada genannten Programmiersprache trug dazu bei, dass Intermetrics kein Interesse daran hatte, diese Arbeit fortzusetzen.

Oh, HAL/S hat noch ein weiteres kleines Problem

Die Schwäche von Hal/S besteht darin, dass es nur verfügbar ist, wenn es auf Mainframe-Computern der Serie IBM 360/370 gehostet wird. Intermetrics hat Hal/S auch auf Modcomp IV und Classic sowie auf Data General Eclipse-Minicomputern gehostet. Die Modcomp-Implementierung wird jedoch nur von JPL verwendet, und die Eclipse-Entwicklung wird nicht mehr verwendet, da Adressraumbeschränkungen die Kompiliergeschwindigkeit auf etwa 30 Zeilen/Minute reduzieren.

Daher ist es nicht verwunderlich, dass es in den frühen 90er Jahren (als PCs auf dem Vormarsch waren) viel billiger war, mehr Standard-Computergeräte zu beschaffen (ich wette, IBM konnte Ada auf mehr Standardhardware ausführen, da sie bereits lieferten) . Astronauten mit Thinkpads zu dieser Zeit ). Interessante Tatsache: Thinkpads mit Linux werden als Schnittstelle zum Stationscomputer verwendet

"Es waren nur die Anwendungsanforderungen", sagte er und beschrieb, wie die Laptop-Software, die in diesen frühen Tagen mit den Befehls- und Kontrollsystemen der Station kommunizierte, so konzipiert war, dass sie auf einem Linux-basierten Betriebssystem ausgeführt werden konnte.

Im Gegensatz dazu fuhr der Neugier- Rover (Anfang der 2000er) auf C

Es führt 2,5 Millionen C-Zeilen auf einem RAD750-Prozessor aus, der von BAE hergestellt wird.

Von der Webseite :

AdaCore-Tools können verwendet werden, um Verifizierungsziele zu erreichen, einschließlich der Einhaltung von Codierungsstandards , Codegenauigkeit ( Vermeidung von Fehlern wie Pufferüberlauf, Ganzzahlüberlauf und Verweise auf nicht initialisierte Variablen) und strukturelle Abdeckungsanalyse bis hin zu MC/DC . Spezialisierte High-Assurance-Laufzeitbibliotheken, darunter eine, die das Ravenscar-Tasking-Profil implementiert, sind einfach genug, um in qualifizierte Systeme integriert zu werden, aber ausdrucksstark genug, um die erforderliche Funktionalität für harte Echtzeit- Weltraumsoftware zu unterstützen. Qualifizierungsmaterial für die Laufzeitbibliotheken kann für den ECSS-Standard entwickelt und an neue Projektkontexte angepasst werden.

C und C++ verhindern diese Fehler nicht (abgesehen von kostspieligen Addons ), und Java ist nicht hart in Echtzeit (abgesehen von nicht standardmäßigen VMs ).

Wenn Leben auf dem Spiel stehen, ist es am besten, Laufzeitfehler und Verzögerungen per Design auszuschließen :

with Ada.Text_IO; use Ada.Text_IO;

procedure Learn is

   subtype Alphabet is Character range 'A' .. 'Z';

begin

   Put_Line ("Learning Ada from " & Alphabet'First & " to " & Alphabet'Last);

end Learn;

Hier kann Alphabet keinen anderen Wert als A bis Z enthalten. Diese ziemlich einzigartige Sprachfunktion half unter anderem einem Team von Studenten, die CubeSat-Mission 2013-2015 abzuschließen :

Als ein Beispiel für Ada im Grundstudium haben Studenten des Vermont Technical College in den USA die SPARK-Sprache (eine formal analysierbare Untergruppe von Ada) verwendet, um die Software für einen CubeSat-Satelliten zu entwickeln, der kürzlich eine erfolgreiche zweijährige Orbitalmission absolviert hat. SPARK wurde aufgrund seiner Zuverlässigkeitsvorteile ausgewählt. Die Studenten hatten keine Vorkenntnisse in Ada, SPARK oder formalen Methoden, konnten sich aber schnell einarbeiten.

Von den zwölf CubeSats von akademischen Einrichtungen, die in den Start einbezogen wurden, war der von Vermont Tech der einzige, der seine Mission erfüllte. Viele der anderen endeten aufgrund von Softwarefehlern. Die Vermont Tech Group führt ihren Erfolg auf den SPARK-Ansatz zurück, der es ihnen beispielsweise ermöglichte, formal die Abwesenheit von Laufzeitfehlern nachzuweisen.

Welche Aspekte von allen möglichen Sprachen zur Auswahl machen Ada zur Wahl der NASA für eine so kritische Anwendung? Wie könnte die Gewichtung zwischen Legacy-Gründen und intrinsischer Eignung aussehen?

• Ada ist eine Sprache , die genau für diese Art von Situation entwickelt wurde , dh fehlerintolerante Echtzeit- und (häufig) eingebettete Systeme, die zur Steuerung kritischer Geräte oder Prozesse verwendet werden

• Adas Entwicklung war von Anfang an viel konzentrierter und strenger gesteuert . Sowohl seine Urheber als auch seine Bewerter waren handverlesene Experten auf dem Gebiet der Sprachentwicklung mit einem starken Pflichtgefühl sowohl ihrem Beruf als auch dem Ada-Projekt gegenüber. So wie die Werte der Westküste Java durchdringen, gab die selbstlose Bescheidenheit von Ichbiah, Dewar und Taft für Ada einen Ton an, der immer noch vorherrscht und einer Organisation wie der NASA gefallen muss.

• Ada verfügt über eine formal definierte Subset-Sprache namens SPARK, die eine einfache Zuordnung eines formal verifizierten Systemdesigns zu seinem Code ermöglicht

• Ada ist eine der schnellsten Sprachen überhaupt, außerdem mit parallelen Prozessoren

• Die Ada-Industrie (Unternehmen wie AdaCore, Altran, Green Hills, Wind River usw. usw.) hat zahlreiche Support-Tools für die kritische Systementwicklung in Ada/SPARK entwickelt

• Es gibt nur wenige fähige Alternativsprachen zu Ada

• Alternative Sprachen wie formal definiertes C verfügen nicht über die gleiche Erfahrungstiefe oder Unterstützung wie Ada/SPARK

Ich habe keine Ahnung, was die detaillierten Systemanforderungen waren oder wie streng die Ausschreibungsrichtlinien in Bezug auf die Gewichtung von Alt- und Eigeneignung waren. Aber es erscheint mir vernünftig, dass Ada/SPARK in beiden Kategorien gut abschneiden würden. Legacy-Faktoren sollten Dinge beinhalten wie

• Die NASA war ein ursprünglicher Sponsor des Ada-Projekts und hatte es von Anfang an auf früheren Systemen verwendet

• Wahrscheinlich größere Vertrautheit des Systembauunternehmens mit Ada/SPARK, Know-how bei der effektiven Bereitstellung seiner Konstrukte für die Anforderungen des neuen kritischen Systems

• Wahrscheinlich bestehende Nutzung von Ada/SPARK durch Subunternehmer, zB eingebettete Systeme für Zusatzgeräte wie Radar, Röntgengeräte usw., für das Projekt und Datenschnittstellen zwischen Haupt- und Subsystemen

Ada ist SGMLvon Programmiersprachen (und Java/C# ist XML). Beide sind in einer neuen Basis für eine Komplettlösung eingebaut. Und beide wurden aufgrund ihrer Komplexität und Kuriosität nicht populär. (Minderheit kennt SGML, aber jeder versteht HTML: Einfachheit ist Stärke.) Wir lernten Ada 1991 und liebten es, obwohl wir von Modula-3 kamen und nicht von Junk Pascal oder C. (Ganz zu schweigen von Assembler.) Ada sah perfekt eingebaut aus Allgemein und im Detail. Aber keiner von uns hat es benutzt, weil die einzige Ada-Umgebung für IBM 360 (oder einen russischen Klon davon) war und viele Jahre lang kein Ada-Compiler für PC erschienen ist. Und es wurde ein "glänzender Diamant in einer Vitrine", theoretisch perfekt, aber unantastbar. Wir haben Code für Sieve of Eratosthenes geschrieben, aber es gab keine Ressourcen, um ihn mit log(log(10e9))-Aufgaben auszuführen. (An diesem Tag zählten sie RAM in Hunderten von KBs. ) Inzwischen kamen gute C++-Umgebungen (mit brauchbaren Klassenbibliotheken!) und die meisten Programmierer verwendeten sie als primäre Plattform, bis Java ein Jahrzehnt später erschien. Und auch für Java gab es keine guten Entwicklungstools, aber brauchbare und auf billigen PCs lauffähige.