ESE Fachwissen
Schneller formal korrekten C-Code durch Benutzung von SPARK erstellen
Autoren: Ingo Houben, Rob Tice, AdaCore
Beitrag - Embedded Software Engineering Kongress 2017
Diese Arbeit zeigt auf, wie formal richtiger Code in der Programmiersprache C erzeugt werden kann, durch einen Ansatz, der die notwendigen Informationen, die man für ein formelles Überprüfen braucht, in der Programmiersprache SPARK selbst unterstützt. Das ist von unserem Standpunkt aus eine neue Sichtweise auf die Software-Entwicklung, bringt viele Vorteile durch die Reduzierung des Entwicklungsaufwandes und spart dadurch Kosten. Das ist speziell auf Kosten bezogen, die bei der Suche nach Fehlern in späten Entwicklungsphasen anfallen. Der Hauptfokus dieser Arbeit besteht in der Beschreibung eines möglichen Arbeitsablaufes, der Kosten durch statische Analyse und formelle Methoden zum Auffinden von potenziellen Laufzeitfehlern in frühen Entwicklungsphasen minimiert. Wir werden uns auf das Schreiben von Programmcode beschränken und Themen wie Safety-Untersuchungen und Anforderungs-Engineering nicht mitberücksichtigen. Wir werden auch keine Beschreibung liefern, wie die formellen Methoden im Einzelnen funktionieren. Das wären zu viele Themen und Details, die auch schon in veröffentlichten Arbeiten zur Verfügung stehen [4] [3].
Das Schreiben von Software für Applikationen wird noch größtenteils von Menschen gemacht. Menschen machen aber Fehler, in den meisten Fällen eher ungewollte und nicht bewusste. Die Statistik zeigt, das bei 1.000 LOC (Lines of Code) ungefähr 10-15 Fehler auftreten. Wenn wir uns jetzt eine sicherheitsrelevante Anwendung mit ~800.000 Zeilen Code vorstellen, dann können wir annehmen, dass 8.000 bis 15.000 Fehler darin enthalten sind. Daher braucht die Entwicklung von sicherheitsrelevanten Anwendungen Wege, um die Anzahl der Fehler drastisch zu reduzieren. Formelle Methoden können hier helfen. Aber das gilt nicht nur für sicherheitsrelevante Anwendungen, es gilt auch für Software in unserem alltäglichen Leben. Wie oft werden Benutzer mit schlecht geschriebener Software konfrontiert? Abstürze oder nicht korrekt implementierte Funktionalität sind an der Tagesordnung. Der Benutzer wird zum Beta-Tester. Der Einsatz von formellen Methoden sollte daher auch auf die alltäglichen Anwendungen übertragen werden, um die Qualität der Software zu erhöhen.
Aber schauen wir erst einmal, welche Möglichkeiten im Moment zur Verfügung stehen, um die Anzahl der Fehler in der Software zu reduzieren.
Ein weit verbreiteter Ansatz ist die Verwendung von Coding-Standards, die jeder Entwickler berücksichtigen muss. MISRA-C ist ein populäres Beispiel. Die Sprachen C und C++ haben viele Möglichkeiten, uneindeutig zu sein, und Richtlinien helfen hier, die mögliche Anzahl von Fehlern zu reduzieren. Es macht den Code außerdem besser lesbar für andere. Im Markt sind Werkzeuge verfügbar, die Programmierern helfen, diese Standards anzuwenden. Aber MISRA-C und auch andere Standards helfen nicht, Fehler in der Software zu finden. Sie beschränken die Sprachen nur und helfen, syntaktische Fehler und uneindeutige Anwendung von Konstrukten zu vermeiden. Selbst wenn die Regeln für einen Standard angewendet werden und syntaktisch korrekter Code vorhanden sind, heißt es noch nicht, dass dieser funktional korrekt arbeitet [7].
Ein weiterer Weg ist die Erhöhung der Anzahl von Tests. Mehr ausgeführte Tests sollten mehr Fehler zum Vorschein bringen - theoretisch. Das Problem bei diesem Ansatz ist, das die Tests meist ausgelegt sind, um das richtige Verhalten zu testen. Moderne Entwicklungsprozesse legen sogar fest, das Test noch vor der Entwicklung der Anwendung geschrieben werden müssen. Das zeigt das Problem auf, denn die Tests werden so geschrieben, dass sie das richtige Verhalten der Anwendung widerspiegeln und sind nicht dafür ausgelegt, versteckte Fehler im Programm zu finden. Daher heißt, dass mit mehr Testen nicht unbedingt das alle Fehler gefunden werden. Tests helfen, mehr Fehler zu finden, wenn diese während der Testphase auftreten. Verschiedene Werkzeuge sind verfügbar, die durch Analyse des Softwarecodes helfen, die notwendigen Tests zu finden. Aber die Benutzung der Werkzeuge und die Ausführung der Tests verbrauchen mehr Zeit im Entwicklungsprozess [6].
Ein weiterer Ansatz könnte die Erhöhung der Anzahl von Reviews sein. Dies erhöht die Möglichkeit, dass Fehler gefunden werden, ist aber immer noch keine Garantie. Da die Arbeit des Reviews von Menschen ausgeführt wird, sind wir wieder beim ersten Problem: Menschen machen Fehler. Reviews sind also nicht die perfekte Lösung. Es erhöht außerdem den Aufwand und verbraucht mehr Arbeitszeit von Mitarbeitern im Entwicklungsprozess. Reviews machen außerdem nur Sinn, wenn die Menge des Codes, der angeschaut wird, klein ist. Wenn sich die Menge des Codes erhöht oder der Code komplex ist, erhöht sich die Wahrscheinlichkeit, dass Probleme übersehen werden.
Der nächste mögliche Ansatz ist die Verwendung von statischen Analysewerkzeugen. Das ist ein Schritt in die richtige Richtung und wird von Herrn Holzmann in seinen zehn Regeln [1] für die Entwicklung von sicherheitsrelevanten System als unerlässlich vorgeschrieben. Aber statische Analysewerkzeuge werden keinen funktionalen Fehler im Code finden. Als Beispiel hierfür können wir eine Funktion betrachten, die Daten in aufsteigender Ordnung sortieren soll, dies aber in absteigender Ordnung macht [8]. Diese Art von Fehler werden statische Analysewerkzeuge nicht finden. In den letzten Jahren ist viel Aufwand betrieben worden, um die Qualität der Algorithmen in den Analysewerkzeugen zu verbessern und die Anzahl der "False-Positive" Meldungen zu reduzieren. "False-Positive" sind Fehler, die die Werkzeuge anzeigen, aber in wirklich gar keine Fehler sind [8]. Dies hat dazu geführt, dass statische Code-Analysewerkzeuge sehr nützlich und hilfreich sind - es hinterlässt aber immer noch die Lücke, funktionelle Fehler zu finden.
Eine Kombination aller vorher genannten Methoden ist die Zertifizierung. Für unterschiedliche Industriebereiche gibt es verschieden Prozeduren, die befolgt werden müssen und dann von einer Zertifizierungsbehörde abgenommen werden. DO178 oder EN 50128 sind Beispiele hierfür. Für ISO 26262 gibt es keine offizielle Zertifizierungsbehörde, trotzdem ist sie ein Schritt in die richtige Richtung. Zertifizierung garantiert einen hohen Standard, dass alle Schritte richtig ausgeführt und die Anzahl der Fehler auf ein Minimum beschränkt wurden. Es ist aber immer noch keine Garantie für die totale Abwesenheit von Fehlern.
Ein anderer Weg zum Auffinden von Fehlern kann die Verwendung von formellen Methoden sein. Diese sind eine Erweiterung der statischen Analysemethoden, aber mit einer anderen Absicht. Statische Analysemethoden werden verwendet, um Fehler in der Software zu finden, formelle Methoden werden verwendet, um vom Anfang an fehlerfreie Software zu entwickeln.
Der Unterschied für den investierten Aufwand zwischen einem testbasierten Ansatz und einem Ansatz, der formelle Methoden verwendet, kann in Abbildung 1 (siehe PDF) gesehen werden.
Die rot gestrichelte Linie zeigt die Kosten für das Finden von Fehlern in der Software über den Zeitraum eines Entwicklungsprojektes; die durchgezogenen Linien zeigen auf, wann wie viele Fehler gefunden werden. In späten Phasen des Entwicklungsprozesses steigen die Kosten für das Beseitigen von Fehlern erheblich im Vergleich zum Finden der Fehler in früheren Phasen. In traditionellen Entwicklungsprozessen mit einem testbasierten Ansatz ist genau das der Fall. Die Probleme werden in der Test- und Integrationsphase gefunden und erzeugen so mehr Kosten, je später sie entdeckt werden. Dies hat zu Kostenexplosionen in Projekten, einer Reduktion von geplanten Funktionalitäten oder sogar zum totalen Scheitern von Projekten geführt. Mit der Verwendung von formellen Methoden kann das Auffinden von Fehlern in frühere Entwicklungsphasen veragert werden; somit können die Kosten signifikant sinken. Es findet ein sogenanntes Frontloading statt. Dies wird auf der rechten Seite von Abbildung 1 (siehe PDF) mit der grünen, nicht gestrichelten Linie dargestellt.
Wenn wir jetzt zu der Überzeugung kommen, dass statische Methoden helfen - welche Optionen sind verfügbar?
Es gibt zwei Wege, formelle Methoden anzuwenden. Auf der einen Seite gibt es den Ansatz von FRAMA-C [2]. Wie der Name schon sagt, arbeitet dieser Ansatz mit der Programmiersprache C. FRAMA-C stellt eine Plattform da, die mit mehreren verschiedenen Werkzeugen den Code formell überprüfen kann. Diese Werkzeuge werden Prover genannt. Um dieses aber den Werkzeugen zu ermöglichen, muss der C-Code mit zusätzlichen Kommentaren versehen werden, die den Provern erklären, wie der Code funktionieren soll. Dies stellt zusätzlichen Aufwand für die Entwickler dar. Es bedeutet auch, dass eine zusätzliche Sprache gelernt werden muss, denn die Kommentare müssen in ACSL (ANSI/ISO C Specification Language) [9] geschrieben werden. Dieser Ansatz hat Erfolge aufgezeigt. Er verlängert aber auch die Entwicklungszeit, weil zusätzlicher Aufwand betrieben werden muss und durch das Einfügen der notwendigen Kommentaremehr Zeit für das Schreiben des Programmes aufgewendet wird.
Anstatt zwei Sprachen zu kombinieren, gibt es einen effizienteren Ansatz der alle notwendigen Konstrukte in einer Sprache enthält. Dieser Ansatz wird mit SPARK [11] verfolgt. Die Unterschiede zwischen FRAMA-C und SPARK können in Abbildung 2 (siehe PDF) gesehen werden. SPARK ist kein Weg um Fehler zu finden, sondern ein Weg die volle Fehlerfreiheit in der Software zu garantieren. Die Mathematik dahinter ist mit der von FRAMA-C vergleichbar und es können die gleichen Prover eingesetzt werden. Nur der Ansatz unterscheidet sich. FRAMA-C arbeitet mit Annotationen in der Form von Kommentaren, SPARK ist eine Untergruppe der Programmiersprache Ada und enthält alle notwendigen Annotationen in der Sprache selber. Wie von dem Experiment von Christophe Garion und Jérôme Hugues gesehen werden kann, erfordert die schwächere Semantik von C doppelt so viele Annotationen und bedeutet daher doppelt so viel Arbeit [2]. Die beiden haben die komplette Fehlerfreiheit in C und SPARK Laufzeitbibliotheken für AADL überprüft, unter der Verwendung von FRAMA-C für die C Version der Bibliothek und SPARK für die ADA Variante, unter Verwendung des Werkzeuges GNATprove. SPARK ist also ein mit weniger Aufwand versehender Ansatz als FRAMA-C, weil der Programmierer in der gleichen Sprache arbeiteten kann, in der er den Code und die Bedingungen zur Überprüfung der korrekten Funktionsweise schreibt.
Ein Hindernis bei der Benutzung von SPARK ist allerdings die Voraussetzung eines Ada 2012 Compilers für die verwendete Hardware. Auch wenn es sehr gute Unterstützung für viele Plattformen gibt, so ist es doch weniger wahrscheinlich einen Ada 2012 Compiler für exotische Plattformen zu finden. Es ist hier wahrscheinlicher einen ISO kompatiblen C-Compiler zur Verfügung zu haben. Aber in dem Fall, dass es keinen Ada Compiler für eine Plattform gibt, ist es trotzdem möglich die Vorteile von SPARK zu benutzen.
Die Lösung die wir hier aufzeigen ist die Verwendung der Sprache C als Zwischenmedium, so dass der von der Hardware verwendete C-Compiler benutzt werden kann um Maschinen Code zu erzeugen. Somit können wir SPARK Code schreiben und die formellen Analysen auf fast jeder Plattform durchführen. Aus Einfachheitsgründen beschränken wir uns bei unseren Analysen auf Daten und Programmflussanalysen. Dies ist vergleichbar mit dem Bronze Level wie im „Implementation Guidance for Adoption of SPARK“ [12] beschrieben. Dieses Konzept kann aber auf den Silber oder Gold Level angehoben werden, um fundamentale Eigenschaften des Codes formell zu überprüfen.
Wir haben in diesem Beispiel auch einen hybriden Ansatz benutzt und SPARK nur für einige Funktionen verwendet und den Rest in Ada oder C gelassen. Der Vorteil dieses Ansatzes liegt in der Beschränkung des Aufwandes auf nur wenige Funktionen die unbedingt fehlerfrei sein müssen und der Rest zum Beispiel aus Legacy Code besteht. Diese bietet die Möglichkeit Schritt-für-Schritt SPARK und formelle Methoden in die Softwareentwicklung zu integrieren.
Unser Beispiel zeigt SPARK 2014 für eine AVR Plattform, im Detail ein Arduino Uno. Das ist eine 16-Bit Plattform für es keinen Ada 2012 Compiler gibt. Ein Nachteil bei der Benutzung von C als Zwischenmedium ist, das man nicht die komplette Stärke von Ada als Programmiersprache verwenden kann. Der verwendete Common Code Generator (CCG) den wir benutzen um C-Code von dem Ada/SPARK Code zu machen, hat nur einen minimalen Satz von Laufzeitkomponenten die mit der Toolkette kommen. Weil wir aber C-Code generieren, den wir dann in der Arduino Build Umgebung in ein Executable umwandeln, können wir das Board Support Package (BSP), die Laufzeitumgebung und die Flash Werkzeuge verwenden, die Arduino mit seiner Plattform bereitstellt.
Workflow-Übersicht
Der Entwicklungsablauf ist in Abbildung 3 (siehe PDF) aufgezeigt. Wir haben SPARK Code geschrieben und mit den SPARK Provern auf Richtigkeit überprüft. Danach haben wir den überprüften SPARK Code mit CCG nach C übersetzt. Dann schieben wir den C-Code in ein Arduino verständliches Bibliotheksformat und generieren die notwendigen Metadaten. Aus dem Arduino Sketch rufen wir dann unseren Applikationseinstiegspunkt auf der vom CCG Binding Schritt erzeugt wurde. Dann führen wir all notwendigen Setup Sequencen aus, die unsere Applikation benötigt. Danach rufen wir von der workloop() vom Arduino Sketch unsere Workloop in der Applikation auf. Dann sagen wir dem Arduino Buildsystem es soll nach der Arduino Library suchen, die als Ausgabe aus dem CCG herauskam. Ist dies geschehen, können wir nun in der Arduino Umgebung die Software bauen und auf die Hardware spielen. Während des Bauens benutzt die Arduino Umgebung einen Satz von Konfigurationsdateien um Makefiles zu generieren und die Arduino Laufzeitumgebung, das BSP, unsere Library und die Main-Loop vom Arduino Sketch zum finalen Binary zu linken, das dann auf das Target übertragen werden kann.
Wie schon vorher erwähnt, verlassen wir uns auf die Arduino Laufzeit Umgebung in unserer SPARK Anwendung. Der beste Weg diese zu tun, ist mit der Benutzung des Pragma Import Features von Ada um CCG zu sagen das wir externe C Funktionen aufrufen. Das ist vergleichbar mit dem External Schlüsselwort von C. In unserer Anwendung verwenden wir viele Dateien aus der Laufzeitumgebung in unserer Applikation. Einige Beispiele dafür werden in Abbildung 4 (siehe PDF) aufgezeigt. In vielen Fällen macht es Sinn die Aufrufe zu C-Funktionen in ein kleines Unterprogramm zu packen um ein stärkeres und robusteres Interface zu erzeugen. Im Vergleich zu einer lockeren Bindung durch einen direkten Aufruf der C-Routine hilft uns der Weg über ein Unterprogramm unsichere C-Operationen aus dem SPARK Code zu separieren und getrennt von unserer SPARK Anwendung zu betrachten.
Die Anwendung in unserem Beispiel ist ein einfacher Roboter der ein reflektierendes Sensoren Cluster benutzt um einer weißen Linie auf schwarzen Untergrund zu folgen. Die Architektur der Software wird in Abbildung 5 (siehe PDF) aufgezeigt. Der Top-Level, sparkzumo package, erzeugt den Einstiegspunkt für die Arduino Applikation. Die Setup Funktion erlaubt Arduino Sketch die Sensoren und Motoren zu initialisieren, sowie eine Kalibrierung des Sensoren Clusters durchzuführen. Die workloop ruft dann die Funktion LineFinder auf.
LineFinder ist der interessanteste Teil der Applikation weil es mehr macht, als nur eine einfache Hardware und Treiber Abstraktion. In diesem Teil nehmen wir die Information vom Sensoren Cluster, berechnen und entscheiden wie der Roboter auf der Linie bleiben soll oder sogar die Linie wiederfinden soll, wenn er sie verloren hat.
Der Datenfluss dieser Funktion kann in Abbildung 5 (siehe PDF) gesehen werden. Der erste Schritt ist, herauszufinden wo sich die Linie im Vergleich zum Roboter befindet. Dies geschieht mit der Funktion ReadLine. Sie kalibriert die Werte vom Sensoren Cluster, filtert das Rauschen und skaliert die Werte basierend auf der Position des Robots. Dann werden die Werte der Sensoren aufaddiert und gemittelt, um einen geschätzten Wert zu erhalten wo sich der Roboter im Vergleich zur Linie befindet. Die Mathematik dahinter kann in Abbildung 6 (siehe PDF) ersehen werden.
Ein Wert von -2500 zeigt an, dass die Linie ganz links vom Roboter ist. Ein Wert von 2500 zeigt, dass die Linie ganz rechts vom Roboter ist. Ein Wert von null sagt, die Linie ist mittig unter dem Roboter. Wenn wir keine Linie unter dem Roboter finden, wollen wir anfangen in immer größer werdenden Kreisen nach ihr zu suchen, solange bis wir sie wiederfinden. Wenn wir die Linie nicht finden, gehen wir in einen Off-Line Error Korrektur Modus der zählt wie oft wir die Linie nicht gefunden haben und verändert die Error Werte basierend auf der Anzahl der Durchläufe. Das heißt jedes Mal, wenn diese Funktion aufgerufen wurde, wird ein etwas größerer Radius gefahren. Die Funktion benutzt den vorherigen Wert und benutzt eine einfache Korrekturschleife erster Ordnung. Idealerweise, wenn der Wert null ist, heißt die Linie ist in der Mitte unter dem Roboter, laufen beide Motoren für links und rechts mit derselben Geschwindigkeit. Wenn der Error Wert abweicht, werden die Motoren so angesteuert, dass sie den Fehler kompensieren und den Roboter wieder auf die Linie bringen.
Basierend auf dieser Beschreibung können wir die Anforderungen für unseren Code in SPARK formulieren um festzustellen, ob der Code auch das macht was er machen soll. Fangen wir bei der ReadLine Funktion an und definieren Anforderungen die auf der Funktionalität beruhen. Wir wissen das die Funktion die Werte des Sensor Clusters ausließt und uns einen Wert zwischen -2500 und 2500 zurückliefern soll. Wir wissen auch, wenn die Linie nicht gefunden wird, erinnert sich der Algorithmus wo er die Linie zuletzt gesehen hat und gibt uns einen passenden Wert zurück. Das ist eine Hilfestellung damit wir die Linie schneller wiederfinden, falls sie verloren gegangen ist. Wir haben somit mindestens eine Variable, LastValue, die bei jedem Durchlauf geupdatet wird. Wir wissen auch, wenn keine Linie gefunden wird dann ist der Rückgabewert -2500 oder 2500. Daraus können wir die in Abbildung 7 (siehe PDF) gezeigte Spezifikation erstellen.
Wir benutzen den Aspekt GLOBAL von SPARK um die Datenabhängigkeit der Funktion zu globalen Variablen zu definieren. Wir erwarten das LastValue gelesen, modifiziert und geschrieben wird. Wir benutzen hier auch POST Bedingungen um die Werte nach der Ausführung der Funktion zu definieren und damit einen Vertrag zwischen dem Aufrufer und dem Aufgerufenen zu definieren. Verträge mit Unterprogrammen garantieren, das die Anforderungen erfüllt werden. Hier zum Beispiel legen wir fest, wenn keine Linie gefunden wird, muss der Rückgabewert der Funktion ein Maximalwert sein, nämlich -2500 oder 2500 vom Typ Robot_Position. Wenn das Unterprogramm diese Anforderung während der Laufzeit nicht erfüllt, wird eine Ausnahme ausgelöst und Fehlerbehandlungsroutinen können ausgeführt werden. SPARK ist anhand dieser Informationen in der Lage die Anforderungen statisch zu überprüfen, bevor das Programm überhaupt ausgeführt wird. Auf diesem Weg können wir die Verträge später entfernen, damit das Binary schlanker und schneller wird, denn wir haben die Korrektheit schon vorab verifiziert.
In der nächsten Funktion, Offline_Correction (Abbildung 8, siehe PDF) modifizieren wir den Wert der Variable Error mit jedem Durchlauf.
Das sorgt dafür, dass der Roboter immer größere Kreise zieht. Wir wissen, dass wir die globale Variable Offline_Offset in der Funktion verändern und die Error Variable in Abhängigkeit der Offline_Offset Variable verändern. Daraus können wir die in der Abbildung 8 (siehe PDF) gezeigte SPARK Spezifikation erstellen. Hier definieren wir eine globale „in out“ Abhängigkeit der Variable Offline_Offset. Das sagt SPARK das wir diese Variable lesen und schreiben werden. Wir verwenden auch den DEPENDS Aspekt um die Datenflussabhängigkeit darzustellen. Mit andere Worten, wir spezifizieren das die Output Variable Error von den Eingabewerten der Variablen Error und Offline_Offset abhängt. Das sagt SPARK das wir Error um den Wert der Variable Offline_Offset modifizieren und dann Offline_Offset selber um eine Konstante ändern. Wir haben auch eine POST Bedingung definiert, die besagt das die Offline_Offset Variable um eine Konstante erhöht werden muss. Mit dieser Datenflussabhängigkeit und dem Vertrag zwischen den Programmen haben wir fast komplett das Verhalten spezifiziert.
Die nächste Funktion, Error_Correct, ist genauso interessant wie die vorhergehende, da wir als Eingabe den Error Wert nehmen und die Geschwindigkeiten für beide Motoren zurückgegeben. Diese Funktion enthält unseren Korrekturalgorithmus. Die Spezifikation für diese Funktion wird in Abbildung 9 (siehe PDF) aufgezeigt.
In dieser Funktion definieren wir zwei Datenabhängigkeiten. Wir haben Default_Speed als Eingabewert und LastError als „in out“ Wert, heißt wir lesen den Wert, verändern und schreiben ihn. SPARK wird sicherstellen, dass wir die Variable Default_Speed in dieser Funktion nicht verändern werden, weil wir sie nur als Eingabewert definiert haben. Wir haben auch Datenflussabhängigkeiten definiert, die besagen, das RightSpeed und LeftSpeed von den Werten Error, LastErorr und DefaultSpeed abhängen. Wir definieren auch als Post Konditionen das die Variable LastError um den Wert Error nach der Ausführung des Unterprograms verändert wird. Die SPARK Werkzeuge können nun überprüfen dass unser Zustand bei jeder Ausführung der Schleife verändert wird und das unsere Daten und Datenflussabhängigkeiten mathematisch korrekt sind. Die Ausführung der SPARK Werkzeuge auf unseren Funktionen zeigt im Report keine Fehler oder Warnungen in der Statischen Analyse. In Abbildung 10 (siehe PDF), markiert durch die gestrichelte Linie, werden die möglichen Ergebnisse eines Durchlaufs von GNATprove gezeigt. Verschiedene Analysen von Datenabhängigkeiten zur LSP Verifikation (Liskov substitution principle) sind möglich. Wenn Überprüfungen erfolgreich durchgelaufen sind, werden keine Ergebnisse zu den Durchläufen angezeigt. Aus den Ergebnissen in Abbildung 10 (siehe PDF) sieht man, Ergebnisse sind mit durchgezogener Linie umrundet, dass keine Daten und Datenfluss-Abhängigkeiten in unserer Software verletzt werden. Es gibt aber noch Initialisierungsfehler, Laufzeitprobleme und einen Fehler in einer Vertragsdefinition zwischen dem Aufrufer und dem Aufgerufenen. Aber diese Fehler beziehen sich nicht auf unsere betrachtete Funktion. Wir können also davon ausgehen das unser Code formal korrekt ist.
Jetzt können wir den SPARK Code an den CCG übergeben, dann mit der Arduino Umgebung kompilieren und danach auf den Roboter übertragen. Da wir die korrekte Funktionalität mit SPARK überprüft haben, sparen wir uns die Test für unsere Funktionen.
Zusammenfassung
Der gezeigte Arbeitsablauf hat die Vorteile von SPARK genutzt um unsere Funktionen auf Daten und Datenflussfehler zu untersuchen und schon während des Schreibens des Codes die Fehlerfreiheit zu garantieren. Wir konnten dann die SPARK Applikation auf eine Hardware übertragen, obwohl für diese kein Ada 2012 Compiler zur Verfügung steht, indem wir als Zwischenschritt C-Code verwendet haben. Somit haben wir formell korrekten C-Code erhalten durch die Verwendung von SPARK und diesen auf die Hardware übertragen.
Ausblick
In den nächsten Schritten werden wir versuchen die noch existierenden Meldungen der SPARK Werkzeuge zu beseitigen und den Steuerungsalgorithmus verbessern. Das Ziel sind zwei miteinander kämpfende Roboter, die sich gegenseitig aus einen begrenzten Spielfeld herausschieben. Möge der bessere Algorithmus gewinnen.
References
[1] Gerard J. Holzmann: The Power of Ten –- http://spinroot.com/gerard/pdf/P10.pdf (2006)
[2] Christophe Garion and Jérôme Hugues: From learning examples to High-Integrity Middleware https://frama-c.com/download/framaCDay/FCSD17/talk/02_Garion_Hugues.pdf (2017)
[3] John W.McComick, Peter C.Chapin : Building High Integrity Applications with SPARK
ISBN: 978-1-107-65684-0
[4] Eduardo Brito: A very short introduction to SPARK: Language, Toolset, Projects, Formal Methods & Certification (2010)
[5] Barry Fagin and Martin Carlisle: Provable Secure DNS: A case Study in Formal Methods
http://ironsides.martincarlisle.com/ICRST2013.pdf (2011)
[6] Barry S. Fargin, Bradley Klanderman, Martin C.Carlisle: Making DNS Server Resistant to Cyber Attacks: An Empirical Study on Formal Methods and Performance
http://ieeexplore.ieee.org/document/8029991/?reload=true (2017)
[7] www.misra.org.uk: MISRA Compliance: 2016 , https://www.misra.org.uk/LinkClick.aspx?fileticket=w_Syhpkf7xA%3D&tabid=57 (2016)
[8] Dr.Paul Anderson : The Use and Limitations of Static-Analysis Tools to Improve Software Quality
https://pdfs.semanticscholar.org/3b8e/a53e62bfc753dabf1deb83be7572d069f6b1.pdf [2008]
[9] Patrick Baudin, Pascal Cuoq, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, Virgile Prevosto: https://frama-c.com/download/acsl_1.4.pdf (2010)
[10] ISO/IEC JTC 1/SC 22/WG 9 Ada Rapporteur Group (ARG): Ada 2012 Language Reference Manual
http://www.ada-auth.org/standards/ada12.html (2012)
[11] AdaCore and Altran UK Ltd: SPARK 2014 Reference Manual
http://docs.adacore.com/spark2014-docs/html/lrm/ (2013-2017)
[12] AdaCore and Thales: Implementation Guidance for the Adoption of SPARK
http://www.adacore.com/uploads/technical-papers/ePDF-ImplementationGuidanceSPARK.pdf (2017)
Unsere Trainings & Coachings
Wollen Sie sich auf den aktuellen Stand der Technik bringen?
Dann informieren Sie sich hier zu Schulungen/ Seminaren/ Trainings/ Workshops und individuellen Coachings von MircoConsult zum Thema Qualität, Safety & Security.
Training & Coaching zu den weiteren Themen unseren Portfolios finden Sie hier.
Qualität, Safety & Security - Fachwissen
Wertvolles Fachwissen zum Thema Qualität, Safety & Security steht hier für Sie zum kostenfreien Download bereit.
Fachwissen zu weiteren Themen unseren Portfolios finden Sie hier.