Autoren: Ingo Houben, Rob Tice, AdaCore 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\u00fcr ein formelles \u00dcberpr\u00fcfen braucht, in der Programmiersprache SPARK selbst unterst\u00fctzt. 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\u00e4ten Entwicklungsphasen anfallen. Der Hauptfokus dieser Arbeit besteht in der Beschreibung eines m\u00f6glichen Arbeitsablaufes, der Kosten durch statische Analyse und formelle Methoden zum Auffinden von potenziellen Laufzeitfehlern in fr\u00fchen Entwicklungsphasen\u00a0minimiert. Wir werden uns auf das Schreiben von Programmcode beschr\u00e4nken und Themen wie Safety-Untersuchungen und Anforderungs-Engineering nicht mitber\u00fccksichtigen. Wir werden auch keine Beschreibung liefern, wie die formellen Methoden im Einzelnen funktionieren. Das w\u00e4ren zu viele Themen und Details, die auch schon in ver\u00f6ffentlichten Arbeiten zur Verf\u00fcgung stehen [4] [3].<\/strong><\/p>\n Das Schreiben von Software f\u00fcr Applikationen wird noch gr\u00f6\u00dftenteils von Menschen gemacht. Menschen machen aber Fehler, in den meisten F\u00e4llen eher ungewollte und nicht bewusste. Die Statistik zeigt, das bei 1.000 LOC (Lines of Code) ungef\u00e4hr 10-15 Fehler auftreten. Wenn wir uns jetzt eine sicherheitsrelevante Anwendung mit ~800.000 Zeilen Code vorstellen, dann k\u00f6nnen 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\u00f6nnen hier helfen. Aber das gilt nicht nur f\u00fcr sicherheitsrelevante Anwendungen, es gilt auch f\u00fcr Software in unserem allt\u00e4glichen Leben. Wie oft werden Benutzer mit schlecht geschriebener Software konfrontiert? Abst\u00fcrze oder nicht korrekt implementierte Funktionalit\u00e4t sind an der Tagesordnung. Der Benutzer wird zum Beta-Tester. Der Einsatz von formellen Methoden sollte daher auch auf die allt\u00e4glichen Anwendungen \u00fcbertragen werden, um die Qualit\u00e4t der Software zu erh\u00f6hen.<\/p>\n Aber schauen wir erst einmal, welche M\u00f6glichkeiten im Moment zur Verf\u00fcgung stehen, um die Anzahl der Fehler in der Software zu reduzieren.<\/p>\n Ein weit verbreiteter Ansatz ist die Verwendung von Coding-Standards, die jeder Entwickler ber\u00fccksichtigen muss. MISRA-C ist ein popul\u00e4res Beispiel. Die Sprachen C und C++ haben viele M\u00f6glichkeiten, uneindeutig zu sein, und Richtlinien helfen hier, die m\u00f6gliche Anzahl von Fehlern zu reduzieren. Es macht den Code au\u00dferdem besser lesbar f\u00fcr andere. Im Markt sind Werkzeuge verf\u00fcgbar, die Programmierern helfen, diese Standards anzuwenden. Aber MISRA-C und auch andere Standards helfen nicht, Fehler in der Software zu finden. Sie beschr\u00e4nken die Sprachen nur und helfen, syntaktische Fehler und uneindeutige Anwendung von Konstrukten zu vermeiden. Selbst wenn die Regeln f\u00fcr einen Standard angewendet werden und syntaktisch korrekter Code vorhanden sind, hei\u00dft es noch nicht, dass dieser funktional korrekt arbeitet [7].<\/p>\n Ein weiterer Weg ist die Erh\u00f6hung der Anzahl von Tests. Mehr ausgef\u00fchrte 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\u00fcssen. Das zeigt das Problem auf, denn die Tests werden so geschrieben, dass sie das richtige Verhalten der Anwendung widerspiegeln und sind nicht daf\u00fcr ausgelegt, versteckte Fehler im Programm zu finden. Daher hei\u00dft, dass mit mehr Testen nicht unbedingt das alle Fehler gefunden werden. Tests helfen, mehr Fehler zu finden, wenn diese w\u00e4hrend der Testphase auftreten. Verschiedene Werkzeuge sind verf\u00fcgbar, die durch Analyse des Softwarecodes helfen, die notwendigen Tests zu finden. Aber die Benutzung der Werkzeuge und die Ausf\u00fchrung der Tests verbrauchen mehr Zeit im Entwicklungsprozess [6].<\/p>\n Ein weiterer Ansatz k\u00f6nnte die Erh\u00f6hung der Anzahl von Reviews sein. Dies erh\u00f6ht die M\u00f6glichkeit, dass Fehler gefunden werden, ist aber immer noch keine Garantie. Da die Arbeit des Reviews von Menschen ausgef\u00fchrt wird, sind wir wieder beim ersten Problem: Menschen machen Fehler. Reviews sind also nicht die perfekte L\u00f6sung. Es erh\u00f6ht au\u00dferdem den Aufwand und verbraucht mehr Arbeitszeit von Mitarbeitern im Entwicklungsprozess. Reviews machen au\u00dferdem nur Sinn, wenn die Menge des Codes, der angeschaut wird, klein ist. Wenn sich die Menge des Codes erh\u00f6ht oder der Code komplex ist, erh\u00f6ht sich die Wahrscheinlichkeit, dass Probleme \u00fcbersehen werden.<\/p>\n Der n\u00e4chste m\u00f6gliche 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\u00fcr die Entwicklung von sicherheitsrelevanten System als unerl\u00e4sslich vorgeschrieben. Aber statische Analysewerkzeuge werden keinen funktionalen Fehler im Code finden. Als Beispiel hierf\u00fcr k\u00f6nnen 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\u00e4t 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\u00fchrt, dass statische Code-Analysewerkzeuge sehr n\u00fctzlich und hilfreich sind – es hinterl\u00e4sst aber immer noch die L\u00fccke, funktionelle Fehler zu finden.<\/p>\n Eine Kombination aller vorher genannten Methoden ist die Zertifizierung. F\u00fcr unterschiedliche Industriebereiche gibt es verschieden Prozeduren, die befolgt werden m\u00fcssen und dann von einer Zertifizierungsbeh\u00f6rde abgenommen werden. DO178 oder EN 50128 sind Beispiele hierf\u00fcr. F\u00fcr ISO 26262 gibt es keine offizielle Zertifizierungsbeh\u00f6rde, trotzdem ist sie ein Schritt in die richtige Richtung. Zertifizierung garantiert einen hohen Standard, dass alle Schritte richtig ausgef\u00fchrt und die Anzahl der Fehler auf ein Minimum beschr\u00e4nkt wurden. Es ist aber immer noch keine Garantie f\u00fcr die totale Abwesenheit von Fehlern.<\/p>\n 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.<\/p>\n Der Unterschied f\u00fcr den investierten Aufwand zwischen einem testbasierten Ansatz und einem Ansatz, der formelle Methoden verwendet, kann in Abbildung 1 (siehe\u00a0PDF<\/a>) gesehen werden.<\/p>\n Die rot gestrichelte Linie zeigt die Kosten f\u00fcr das Finden von Fehlern in der Software \u00fcber den Zeitraum eines Entwicklungsprojektes; die durchgezogenen Linien zeigen auf, wann wie viele Fehler gefunden werden. In sp\u00e4ten Phasen des Entwicklungsprozesses steigen die Kosten f\u00fcr das Beseitigen von Fehlern erheblich im Vergleich zum Finden der Fehler in fr\u00fcheren 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\u00e4ter sie entdeckt werden. Dies hat zu Kostenexplosionen in Projekten, einer Reduktion von geplanten Funktionalit\u00e4ten oder sogar zum totalen Scheitern von Projekten gef\u00fchrt. Mit der Verwendung von formellen Methoden kann das Auffinden von Fehlern in fr\u00fchere Entwicklungsphasen veragert werden; somit k\u00f6nnen die Kosten signifikant sinken. Es findet ein sogenanntes Frontloading statt. Dies wird auf der rechten Seite von Abbildung 1 (siehe\u00a0PDF<\/a>) mit der gr\u00fcnen, nicht gestrichelten Linie dargestellt.<\/p>\n Wenn wir jetzt zu der \u00dcberzeugung kommen, dass statische Methoden helfen – welche Optionen sind verf\u00fcgbar?<\/p>\n 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 \u00fcberpr\u00fcfen kann. Diese Werkzeuge werden Prover genannt. Um dieses aber den Werkzeugen zu erm\u00f6glichen, muss der C-Code mit zus\u00e4tzlichen Kommentaren versehen werden, die den Provern erkl\u00e4ren, wie der Code funktionieren soll. Dies stellt zus\u00e4tzlichen Aufwand f\u00fcr die Entwickler dar. Es bedeutet auch, dass eine zus\u00e4tzliche Sprache gelernt werden muss, denn die Kommentare m\u00fcssen in ACSL (ANSI\/ISO C Specification Language) [9] geschrieben werden. Dieser Ansatz hat Erfolge aufgezeigt. Er verl\u00e4ngert aber auch die Entwicklungszeit, weil zus\u00e4tzlicher Aufwand betrieben werden muss und durch das Einf\u00fcgen der notwendigen Kommentaremehr Zeit f\u00fcr das Schreiben des Programmes aufgewendet wird.<\/p>\n Anstatt zwei Sprachen zu kombinieren, gibt es einen effizienteren Ansatz der alle notwendigen Konstrukte in einer Sprache enth\u00e4lt. Dieser Ansatz wird mit SPARK [11] verfolgt. Die Unterschiede zwischen FRAMA-C und SPARK k\u00f6nnen in Abbildung 2 (siehe\u00a0PDF<\/a>) 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\u00f6nnen 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\u00e4lt alle notwendigen Annotationen in der Sprache selber. Wie von dem Experiment von Christophe Garion und J\u00e9r\u00f4me Hugues gesehen werden kann, erfordert die schw\u00e4chere 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\u00fcr AADL \u00fcberpr\u00fcft, unter der Verwendung von FRAMA-C f\u00fcr die C Version der Bibliothek und SPARK f\u00fcr 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 \u00dcberpr\u00fcfung der korrekten Funktionsweise schreibt.<\/p>\n Ein Hindernis bei der Benutzung von SPARK ist allerdings die Voraussetzung eines Ada 2012 Compilers f\u00fcr die verwendete Hardware. Auch wenn es sehr gute Unterst\u00fctzung f\u00fcr viele Plattformen gibt, so ist es doch weniger wahrscheinlich einen Ada 2012 Compiler f\u00fcr exotische Plattformen zu finden. Es ist hier wahrscheinlicher einen ISO kompatiblen C-Compiler zur Verf\u00fcgung zu haben. Aber in dem Fall, dass es keinen Ada Compiler f\u00fcr eine Plattform gibt, ist es trotzdem m\u00f6glich die Vorteile von SPARK zu benutzen.<\/p>\n Die L\u00f6sung 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\u00f6nnen wir SPARK Code schreiben und die formellen Analysen auf fast jeder Plattform durchf\u00fchren. Aus Einfachheitsgr\u00fcnden beschr\u00e4nken wir uns bei unseren Analysen auf Daten und Programmflussanalysen. Dies ist vergleichbar mit dem Bronze Level wie im \u201eImplementation Guidance for Adoption of SPARK\u201c [12] beschrieben. Dieses Konzept kann aber auf den Silber oder Gold Level angehoben werden, um fundamentale Eigenschaften des Codes formell zu \u00fcberpr\u00fcfen.<\/p>\n Wir haben in diesem Beispiel auch einen hybriden Ansatz benutzt und SPARK nur f\u00fcr einige Funktionen verwendet und den Rest in Ada oder C gelassen. Der Vorteil dieses Ansatzes liegt in der Beschr\u00e4nkung des Aufwandes auf nur wenige Funktionen die unbedingt fehlerfrei sein m\u00fcssen und der Rest zum Beispiel aus Legacy Code besteht. Diese bietet die M\u00f6glichkeit Schritt-f\u00fcr-Schritt SPARK und formelle Methoden in die Softwareentwicklung zu integrieren.<\/p>\n Unser Beispiel zeigt SPARK 2014 f\u00fcr eine AVR Plattform, im Detail ein Arduino Uno. Das ist eine 16-Bit Plattform f\u00fcr es keinen Ada 2012 Compiler gibt. Ein Nachteil bei der Benutzung von C als Zwischenmedium ist, das man nicht die komplette St\u00e4rke 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\u00f6nnen wir das Board Support Package (BSP), die Laufzeitumgebung und die Flash Werkzeuge verwenden, die Arduino mit seiner Plattform bereitstellt.<\/p>\n Der Entwicklungsablauf ist in\u00a0Abbildung 3<\/em>\u00a0(siehe\u00a0PDF<\/a>) aufgezeigt. Wir haben SPARK Code geschrieben und mit den SPARK Provern auf Richtigkeit \u00fcberpr\u00fcft. Danach haben wir den \u00fcberpr\u00fcften SPARK Code mit CCG nach C \u00fcbersetzt. Dann schieben wir den C-Code in ein Arduino verst\u00e4ndliches 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\u00fchren wir all notwendigen Setup Sequencen aus, die unsere Applikation ben\u00f6tigt. 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\u00f6nnen wir nun in der Arduino Umgebung die Software bauen und auf die Hardware spielen. W\u00e4hrend 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 \u00fcbertragen werden kann.<\/p>\n Wie schon vorher erw\u00e4hnt, 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\u00fcsselwort von C. In unserer Anwendung verwenden wir viele Dateien aus der Laufzeitumgebung in unserer Applikation. Einige Beispiele daf\u00fcr werden in Abbildung 4 (siehe\u00a0PDF<\/a>) aufgezeigt. In vielen F\u00e4llen macht es Sinn die Aufrufe zu C-Funktionen in ein kleines Unterprogramm zu packen um ein st\u00e4rkeres und robusteres Interface zu erzeugen. Im Vergleich zu einer lockeren Bindung durch einen direkten Aufruf der C-Routine hilft uns der Weg \u00fcber ein Unterprogramm unsichere C-Operationen aus dem SPARK Code zu separieren und getrennt von unserer SPARK Anwendung zu betrachten.<\/p>\n Die Anwendung in unserem Beispiel ist ein einfacher Roboter der ein reflektierendes Sensoren Cluster benutzt um einer wei\u00dfen Linie auf schwarzen Untergrund zu folgen. Die Architektur der Software wird in Abbildung 5 (siehe\u00a0PDF<\/a>) aufgezeigt. Der Top-Level, sparkzumo package, erzeugt den Einstiegspunkt f\u00fcr die Arduino Applikation. Die Setup Funktion erlaubt Arduino Sketch die Sensoren und Motoren zu initialisieren, sowie eine Kalibrierung des Sensoren Clusters durchzuf\u00fchren. Die workloop ruft dann die Funktion LineFinder auf.<\/p>\n 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.<\/p>\n Der Datenfluss dieser Funktion kann in Abbildung 5 (siehe\u00a0PDF<\/a>) 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\u00e4tzten Wert zu erhalten wo sich der Roboter im Vergleich zur Linie befindet. Die Mathematik dahinter kann in Abbildung 6 (siehe\u00a0PDF<\/a>) ersehen werden.<\/p>\n 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\u00f6\u00dfer 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\u00e4hlt wie oft wir die Linie nicht gefunden haben und ver\u00e4ndert die Error Werte basierend auf der Anzahl der Durchl\u00e4ufe. Das hei\u00dft jedes Mal, wenn diese Funktion aufgerufen wurde, wird ein etwas gr\u00f6\u00dferer Radius gefahren. Die Funktion benutzt den vorherigen Wert und benutzt eine einfache Korrekturschleife erster Ordnung. Idealerweise, wenn der Wert null ist, hei\u00dft die Linie ist in der Mitte unter dem Roboter, laufen beide Motoren f\u00fcr 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.<\/p>\n Basierend auf dieser Beschreibung k\u00f6nnen wir die Anforderungen f\u00fcr 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\u00e4t beruhen. Wir wissen das die Funktion die Werte des Sensor Clusters auslie\u00dft und uns einen Wert zwischen -2500 und 2500 zur\u00fcckliefern 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\u00fcck. 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\u00fcckgabewert -2500 oder 2500. Daraus k\u00f6nnen wir die in Abbildung 7 (siehe\u00a0PDF<\/a>) gezeigte Spezifikation erstellen.<\/p>\n Wir benutzen den Aspekt GLOBAL von SPARK um die Datenabh\u00e4ngigkeit 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\u00fchrung der Funktion zu definieren und damit einen Vertrag zwischen dem Aufrufer und dem Aufgerufenen zu definieren. Vertr\u00e4ge mit Unterprogrammen garantieren, das die Anforderungen erf\u00fcllt werden. Hier zum Beispiel legen wir fest, wenn keine Linie gefunden wird, muss der R\u00fcckgabewert der Funktion ein Maximalwert sein, n\u00e4mlich -2500 oder 2500 vom Typ Robot_Position. Wenn das Unterprogramm diese Anforderung w\u00e4hrend der Laufzeit nicht erf\u00fcllt, wird eine Ausnahme ausgel\u00f6st und Fehlerbehandlungsroutinen k\u00f6nnen ausgef\u00fchrt werden. SPARK ist anhand dieser Informationen in der Lage die Anforderungen statisch zu \u00fcberpr\u00fcfen, bevor das Programm \u00fcberhaupt ausgef\u00fchrt wird. Auf diesem Weg k\u00f6nnen wir die Vertr\u00e4ge sp\u00e4ter entfernen, damit das Binary schlanker und schneller wird, denn wir haben die Korrektheit schon vorab verifiziert.<\/p>\n In der n\u00e4chsten Funktion, Offline_Correction (Abbildung 8, siehe\u00a0PDF<\/a>) modifizieren wir den Wert der Variable Error mit jedem Durchlauf.<\/p>\n Das sorgt daf\u00fcr, dass der Roboter immer gr\u00f6\u00dfere Kreise zieht. Wir wissen, dass wir die globale Variable Offline_Offset in der Funktion ver\u00e4ndern und die Error Variable in Abh\u00e4ngigkeit der Offline_Offset Variable ver\u00e4ndern. Daraus k\u00f6nnen wir die in der Abbildung 8 (siehe\u00a0PDF<\/a>) gezeigte SPARK Spezifikation erstellen. Hier definieren wir eine globale \u201ein out\u201c Abh\u00e4ngigkeit der Variable Offline_Offset. Das sagt SPARK das wir diese Variable lesen und schreiben werden. Wir verwenden auch den DEPENDS Aspekt um die Datenflussabh\u00e4ngigkeit darzustellen. Mit andere Worten, wir spezifizieren das die Output Variable Error von den Eingabewerten der Variablen Error und Offline_Offset abh\u00e4ngt. Das sagt SPARK das wir Error um den Wert der Variable Offline_Offset modifizieren und dann Offline_Offset selber um eine Konstante \u00e4ndern. Wir haben auch eine POST Bedingung definiert, die besagt das die Offline_Offset Variable um eine Konstante erh\u00f6ht werden muss. Mit dieser Datenflussabh\u00e4ngigkeit und dem Vertrag zwischen den Programmen haben wir fast komplett das Verhalten spezifiziert.<\/p>\n Die n\u00e4chste Funktion, Error_Correct, ist genauso interessant wie die vorhergehende, da wir als Eingabe den Error Wert nehmen und die Geschwindigkeiten f\u00fcr beide Motoren zur\u00fcckgegeben. Diese Funktion enth\u00e4lt unseren Korrekturalgorithmus. Die Spezifikation f\u00fcr diese Funktion wird in Abbildung 9 (siehe\u00a0PDF<\/a>) aufgezeigt.<\/p>\n In dieser Funktion definieren wir zwei Datenabh\u00e4ngigkeiten. Wir haben Default_Speed als Eingabewert und LastError als \u201ein out\u201c Wert, hei\u00dft wir lesen den Wert, ver\u00e4ndern und schreiben ihn. SPARK wird sicherstellen, dass wir die Variable Default_Speed in dieser Funktion nicht ver\u00e4ndern werden, weil wir sie nur als Eingabewert definiert haben. Wir haben auch Datenflussabh\u00e4ngigkeiten definiert, die besagen, das RightSpeed und LeftSpeed von den Werten Error, LastErorr und DefaultSpeed abh\u00e4ngen. Wir definieren auch als Post Konditionen das die Variable LastError um den Wert Error nach der Ausf\u00fchrung des Unterprograms ver\u00e4ndert wird. Die SPARK Werkzeuge k\u00f6nnen nun \u00fcberpr\u00fcfen dass unser Zustand bei jeder Ausf\u00fchrung der Schleife ver\u00e4ndert wird und das unsere Daten und Datenflussabh\u00e4ngigkeiten mathematisch korrekt sind. Die Ausf\u00fchrung der SPARK Werkzeuge auf unseren Funktionen zeigt im Report keine Fehler oder Warnungen in der Statischen Analyse. In Abbildung 10 (siehe\u00a0PDF<\/a>), markiert durch die gestrichelte Linie, werden die m\u00f6glichen Ergebnisse eines Durchlaufs von GNATprove gezeigt. Verschiedene Analysen von Datenabh\u00e4ngigkeiten zur LSP Verifikation (Liskov substitution principle) sind m\u00f6glich. Wenn \u00dcberpr\u00fcfungen erfolgreich durchgelaufen sind, werden keine Ergebnisse zu den Durchl\u00e4ufen angezeigt. Aus den Ergebnissen in Abbildung 10 (siehe\u00a0PDF<\/a>) sieht man, Ergebnisse sind mit durchgezogener Linie umrundet, dass keine Daten und Datenfluss-Abh\u00e4ngigkeiten 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\u00f6nnen also davon ausgehen das unser Code formal korrekt ist.<\/p>\n Jetzt k\u00f6nnen wir den SPARK Code an den CCG \u00fcbergeben, dann mit der Arduino Umgebung kompilieren und danach auf den Roboter \u00fcbertragen. Da wir die korrekte Funktionalit\u00e4t mit SPARK \u00fcberpr\u00fcft haben, sparen wir uns die Test f\u00fcr unsere Funktionen.<\/p>\n Der gezeigte Arbeitsablauf hat die Vorteile von SPARK genutzt um unsere Funktionen auf Daten und Datenflussfehler zu untersuchen und schon w\u00e4hrend des Schreibens des Codes die Fehlerfreiheit zu garantieren. Wir konnten dann die SPARK Applikation auf eine Hardware \u00fcbertragen, obwohl f\u00fcr diese kein Ada 2012 Compiler zur Verf\u00fcgung 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 \u00fcbertragen.<\/p>\n In den n\u00e4chsten Schritten werden wir versuchen die noch existierenden Meldungen der SPARK Werkzeuge zu beseitigen und den Steuerungsalgorithmus verbessern. Das Ziel sind zwei miteinander k\u00e4mpfende Roboter, die sich gegenseitig aus einen begrenzten Spielfeld herausschieben. M\u00f6ge der bessere Algorithmus gewinnen.<\/p>\n [1] Gerard J. Holzmann: The Power of Ten \u2013-\u00a0https:\/\/spinroot.com\/gerard\/pdf\/P10.pdf<\/a>\u00a0(2006)<\/p>\n [2] Christophe Garion and J\u00e9r\u00f4me Hugues: From learning examples to High-Integrity Middleware\u00a0https:\/\/frama-c.com\/download\/framaCDay\/FCSD17\/talk\/02_Garion_Hugues.pdf<\/a>\u00a0 (2017)<\/p>\n [3] John W.McComick, Peter C.Chapin : Building High Integrity Applications with SPARK [4] Eduardo Brito: A very short introduction to SPARK: Language, Toolset, Projects, Formal Methods & Certification (2010)<\/p>\n [5] Barry Fagin and Martin Carlisle: Provable Secure DNS: A case Study in Formal Methods [6] Barry S. Fargin, Bradley Klanderman, Martin C.Carlisle:\u00a0 Making DNS Server Resistant to Cyber Attacks: An Empirical Study on Formal Methods and Performance [7]\u00a0www.misra.org.uk<\/a>: MISRA Compliance: 2016 ,\u00a0https:\/\/www.misra.org.uk\/LinkClick.aspx?fileticket=w_Syhpkf7xA%3D&tabid=57<\/a>\u00a0 (2016)<\/p>\n [8] Dr.Paul Anderson\u00a0: The Use and Limitations of Static-Analysis Tools to Improve Software Quality [9] Patrick Baudin, Pascal Cuoq, Jean-Christophe Filli\u00e2tre, Claude March\u00e9, Benjamin Monate, Yannick Moy, Virgile Prevosto:\u00a0https:\/\/frama-c.com\/download\/acsl_1.4.pdf<\/a>\u00a0 (2010)<\/p>\n [10] ISO\/IEC JTC 1\/SC 22\/WG 9 Ada Rapporteur Group (ARG): Ada 2012 Language Reference Manual [11]\u00a0 AdaCore and Altran UK Ltd: SPARK 2014 Reference Manual [12] AdaCore and Thales: Implementation Guidance for the Adoption of SPARK Beitrag als PDF downloaden<\/strong><\/a><\/p>\n Wollen Sie sich auf den aktuellen Stand der Technik bringen?<\/strong><\/p>\n Dann informieren Sie sich\u00a0hier<\/strong>\u00a0<\/a>zu Schulungen\/ Seminaren\/ Trainings\/ Workshops und individuellen Coachings von MircoConsult zum Thema\u00a0Qualit\u00e4t, Safety & Security<\/strong>.<\/p>\n Wertvolles Fachwissen zum Thema Qualit\u00e4t, Safety & Security steht\u00a0hier\u00a0<\/a>f\u00fcr Sie zum kostenfreien Download bereit.<\/p>\n
\n<\/strong><\/p>\nBeitrag – Embedded Software Engineering Kongress 2017<\/h3>\n
Workflow-\u00dcbersicht<\/h2>\n
Zusammenfassung<\/h2>\n
Ausblick<\/h2>\n
References<\/h2>\n
\nISBN: 978-1-107-65684-0<\/p>\n
\nhttps:\/\/ironsides.martincarlisle.com\/ICRST2013.pdf<\/a>\u00a0 (2011)<\/p>\n
\nhttps:\/\/ieeexplore.ieee.org\/document\/8029991\/?reload=true<\/a>\u00a0(2017)<\/p>\n
\nhttps:\/\/pdfs.semanticscholar.org\/3b8e\/a53e62bfc753dabf1deb83be7572d069f6b1.pdf<\/a>\u00a0 [2008]<\/p>\n
\nhttps:\/\/www.ada-auth.org\/standards\/ada12.html<\/a>\u00a0(2012)<\/p>\n
\nhttps:\/\/docs.adacore.com\/spark2014-docs\/html\/lrm\/<\/a>\u00a0 (2013-2017)<\/p>\n
\nhttps:\/\/www.adacore.com\/uploads\/technical-papers\/ePDF-ImplementationGuidanceSPARK.pdf<\/a>\u00a0(2017)<\/p>\n
\nUnsere Trainings & Coachings<\/h2>\n
\nTraining & Coaching zu den weiteren Themen unseren Portfolios finden Sie\u00a0hier<\/a>.<\/strong><\/p>\n
\nQualit\u00e4t, Safety & Security – Fachwissen<\/h2>\n