Softwareverifikation in der Industrie I Hat jemand irgendwelche Erfahrungen?

Simon.F

Neues Mitglied
Hallo zusammen,

ich arbeite derzeit mit einer universitären Forschungsgruppe zusammen. Wir untersuchen den praktischen Einsatz von Software-Verifikationswerkzeugen in der Industrie.

Uns interessiert insbesondere, ob es einen Markt für mathematische Werkzeuge (z. B. formal verification, model checking, static analysis) gibt und wie diese in der Praxis eingesetzt werden – beispielsweise in der Qualitätssicherung, der Softwareentwicklung oder in Compliance-intensiven Branchen wie der Automobil- oder Luft- und Raumfahrt.

Daher wollte ich fragen:

– Wie stellen Unternehmen derzeit sicher, dass Sicherheits- und Qualitätsstandards für Software eingehalten werden?

– Was sind die Beweggründe für ihren Einsatz (Sicherheit, Zertifizierungen, Kostensenkung usw.)?

Auch kurze Antworten oder anekdotische Einblicke sind sehr hilfreich. Für Referenzen oder Fallbeispiele wären wir dankbar!

Vielen Dank im Voraus,

Simon
 

meientau

Mitglied
Statische Codeanalyse (lint) und dynamische Codeanalyse (leak detection) sind für die von dir genannten Felder Automotive, Aviation, Space, und auch Medizintechnik von den Normen gefordert. Bei uns (Medizintechnik) ist z.B. IEC 62304 wichtig, auch wenn ich gerade nicht auswendig weiß, welche Maßnahmen da konkret gefordert sind, oder ob das über Ecken reinkommt.
Formale Verifikation habe ich vor 30 Jahren im Studium mal gesehen und damals war das angeblich der heiße Scheiß für z.B. Signalanlagen - keine Ahnung, wie sich das entwickelt hat. Ich glaube eigentlich das Weizenbaum recht hatte - es gibt Systeme, die sind so komplex, dass man sie einfach gar nicht bauen darf, weil das nicht sicher geht ... Und inzwischen sind die Systeme, die wir bauen, um das tausendfache komplizierter, als alles, was Weizenbaum zu Lebzeiten noch gesehen hat. Trotzdem machen wir das, und das geht wohl nicht mehr formal, aber die anderen Maßnahmen "reichen" uns. Wer auch immer das gerade entscheidet. Siehe Boeing ...
Model Checking machen wir zumindest in dem Medizintechnik-Unternehmen, in dem ich arbeite, so nicht, alles - Risikoanalyse und Anforderungen - leiten sich natürlich vom Intended Use ab, und daraus dann die Maßnahmen zur Verifikation und Validierung.
Die Masse unserer Verifikation sind handgeschriebene Tests - automatisiert als Unit-Tests, automatisierte Integrationstests, automatisierte GUI-Tests, und immer noch ein haufen manueller GUI-Tests, weil man nicht alles so einfach automatisieren kann, wenn man Geräte und Modelle dazu braucht, z.B. Plastikknochen oder so. Dabei müssen wir bei einem Audit nicht nur die Ergebnisse zeigen, sondern auch die Begründung, warum diese Tests in angemessenem Verhältnis zum Produktrisiko stehen, sowohl in Umfang als auch in Test-Tiefe (d.h. wie tief denken wir uns in einem White-Box-Test vom bestimmungsgemäßen Gebrauch (Intended Use) in den Code rein).
Bin gespannt auf antworten aus anderen Feldern :)
 

White_Fox

Top Contributor
Es gibt einen Markt, und der wird schon längst bedient.

Automotive ist da das bekannteste Beispiel. In der Luftfahrt kommt C mittlerweile auch zum Einsatz. Boeing ist im Zuge der 737MAX-Untersuchungen negativ dadurch aufgefallen, daß sie die Programmierung des MCAS (das die zwei Maschinen abgestürzt hat) an Billiginder ausgelagert hat.

Eigentlich wurden für wichtige Dinge, wo Menschenleben dran hängen, Sprachen wie Ada entwickelt.

C ist zwar eine altehrwürdige Krüppelsprache, mit der man eigentlich gar nichts wichtiges mehr machen sollte. Aber jeder Depp kann halt in C programmieren, Programmierer für Ada sind weitaus seltener. Und so arbeiten die Firmen mit dem, was sie bekommen können...
 

Oneixee5

Top Contributor
C ist zwar eine altehrwürdige Krüppelsprache, mit der man eigentlich gar nichts wichtiges mehr machen sollte. Aber jeder Depp kann halt in C programmieren,
Mann o Mann ...

Hier sind einige Beispiele für Software in purem C:
  • Betriebssystemkerne:
    Viele Betriebssysteme, insbesondere Unix-basierte wie Linux und macOS, haben ihren Kern in C geschrieben.
  • Eingebettete Systeme:
    C wird oft für die Programmierung von Mikrocontrollern und anderen eingebetteten Systemen verwendet, da es eine effiziente Kontrolle über Hardware erlaubt.


  • Compiler und Interpreter:
    Viele Compiler und Interpreter, auch für andere Programmiersprachen, werden in C geschrieben, um die Grundlage für die Übersetzung und Ausführung von Code zu schaffen.


  • Systemdienstprogramme:
    C ist die bevorzugte Sprache für die Erstellung von Systemwerkzeugen, die zur Verwaltung und Wartung von Betriebssystemen benötigt werden, wie z.B. Dateisystemtools oder Netzwerkdienste.

  • Datenbanksysteme:
    Einige Datenbankmanagementsysteme, wie z.B. MySQL, haben wichtige Komponenten in C implementiert, um eine hohe Leistung zu gewährleisten.


  • Grafikbibliotheken:
    Manche Grafikbibliotheken, die in anderen Programmiersprachen verwendet werden, haben Kernfunktionen in C geschrieben.


  • Spieleentwicklung:
    Auch wenn viele Spiele heute mit höheren Abstraktionen entwickelt werden, gibt es immer noch Bereiche in der Spieleentwicklung, in denen C verwendet wird, z.B. für Hardwarenahe Programmierung oder Spiele-Engines.


  • Netzwerkprogrammierung:
    C wird oft für die Entwicklung von Netzwerkprotokollen und Anwendungen eingesetzt, die eine hohe Leistung und Kontrolle über die Netzwerkkommunikation erfordern.
 

Neue Themen


Oben