Formal korrekten C-Code durch Benutzung von SPARK programmieren

Anbieter zum Thema

MicroConsult Academy GmbH

AdaCore

Ein Beispiel zur Erzeugung von formal richtigem C-Code mit SPARK

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.

Bildergalerie

Bildergalerie mit 9 Bildern

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 Bild 3 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 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 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 Bild 5 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 der folgenden Formel 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 Bild 6 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.

Wert mit jedem Durchlauf modifizieren

In der nächsten Funktion, Offline_Correction (Bild 7) 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 Bild 7 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 Bild 8 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, 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 Bild 9 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.

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 durch die Verwendung von SPARK formell korrekten C-Code erhalten und diesen auf die Hardware übertragen.

C programmieren: Kontrollstrukturen und Funktionen in C

Codegenerierung – was man damit (nicht) machen kann

Literaturverweise

[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)

* Ingo Houben ist Technischer Account Manager und Business Development Manager bei AdaCore.

* Rob Tice arbeitet als Technischer Account Manager bei AdaCore US.

(ID:45474853)