MP-SS18-02

Aus Verteilte Systeme - Wiki
Wechseln zu: Navigation, Suche

Masterprojekt - Formale Verifikation eines Betriebssystem-Schedulers


Projektrahmen

Dieses Projekt gliedert sich in den HSRM Beitrag zum europäischen Forschungsprojekt Aquas ein.

Aquas logo.png Europa logo.jpg Bildung forschung logo.jpg Dopsy logo.svg


  • Ausgangsbasis bildet ein in C entwickeltes Betriebsystem mit der Bezeichnung Marron (von A. Züpke Dipl. Ing. (FH))
  • Konkrete Zielsetzung für dieses Projekt ist die Migration und Verifikation des Schedulers
  • Die C-Quellen von Marron werden im Projektverlauf nach SPARK2014 und Ada überführt
    • Im Zuge der Migration soll die Möglichkeit einer Modularisierung eruiert werden
    • Integration einer vorhandenen mit SPARK verifizierten Queue (von O. Dedi M.Sc.)
  • Anreicherung des Codes mit Contracts
  • Verifikation des Codes mittels des SPARK Toolings
  • Entwicklung einer Simulation zur Demonstration und Erprobung der umgesetzten Portierung

Projektgliederung

Das Projekt wurde in folgende Abschnitte aufgeteilt:

Projektplan_Verifikation_Systemsoftware

Das Projekt wurde in Rahmen des Masterprojektes Studiengang Master Informatik (PO2010) durchgeführt und besaß somit einen zeitlichen Rahmen von 450 Stunden. Eine detailliertere Verteilung ist im Abschnitt Zeitverteilung zu finden.


Hinweise zur Dokumentation

Light bulb.png Die Hinweis-Boxen stellen Erkenntnisse des Projektes dar
Document.png Die Notiz-Boxen enthalten allgemeine Hinweise zum Umgang mit SPARK/Ada oder zum C-Code


Einarbeitung Ada / SPARK

Das Projekte startete mit der Einarbeitung in die Programmiersprachen Ada und SPARK2014, da der Autor dieses Artikels zu Projektbeginn keinerlei Kenntnisse in diesem Bereich mitbrachte. Die Einarbeitung in Ada erfolgte mit Hilfe des Buches "Programming in Ada 2012" von John Barnes und für die Einarbeitung in SPARK 2014 wurde das Buch "Building High Integrity Applications with SPARK" von John W Mccormick verwendet.

Light bulb.png Empfehlung: Wenn an diesem Projekt ohne Vorkenntnisse im Bereich Ada/SPARK gearbeitet wird, dann sollte direkt mit dem Buch "Building High Integrity Applications with SPARK" eingestiegen werden. Diese enthält bereits alle notwendigen (und auch einsetzbaren) Ada Grundkenntnisse. Durch die SPARK Einschränkung profitiert man nicht von der vollen Ada Tiefe/Mächtigkeit die das "Programming in Ada 2012" enthält.


Analyse

In der Analyse wurde sich der C-Code des Marron Betriebssystems betrachtet. Dies beinhaltet:

  • Sichten der vorhanden Sourcen und erstellen einer groben Übersicht
  • Ablauf des bisherigen Systems
  • Festhalten der Zusammenhänge zwischen den einzelnen Komponenten (als Komponente wird in diesem Kontext bspw. der C-Scheduler bezeichnet, bestehend aus sched.c, sched.h)

Darüberhinaus wird in diesem Kapitel auf ein projektähnliches Paper eingegangen, wobei Gemeinsamkeiten und Unterschiede herausgearbeitet wurden.

[weiterlesen]

Migration

Diese Phase beschäftigt sich mit dem ersten praktischen Anteil (wenn man an dieser Stelle die Beispielprogramme der Einarbeitungsphase vernachlässigt) des Projektes. Hierbei wurde in drei Schritten vorgegangen:

  • Überführung der C Header Dateien (.h) zu SPARK Spezifikationsdateien (.ads) für die Komponenten sched und thread
  • Überführung der C Source Dateien (.c) zu SPARK Body Dateien (.adb) für die Komponenten sched und thread
  • Partielle Migration der kernel_main.c zu kernel_main.adb um eine erste Ausgangsbasis zu haben die zuvor migrierten Funktionen zu testen

In diesem Abschnitt wird ebenfalls auf die Problematik eingegangen, dass SPARK keine Pointer zulässt.

[weiterlesen]

Verifikation

Im Abschnitt Verifikation wird der Prozess beschrieben, der angewendet wurde, um die im C-Code vorhandenen Assertions in SPARK/Ada Contracts zu überführen.

Desweiteren wurde herausgearbeitet:

  • Auslagerung der Verifikation in eigene Packages, um die Spezifikationsdateien kompakt und übersichtlich zu halten
  • Abstract States und die damit verbunden Probleme
  • Vorgehen mit Verifkationsfehlern

[weiterlesen]

Weitere generelle Erkenntnisse

Light bulb.png Regelmäßiges Ausführen von GNATProve reduziert den Analyseaufwand im Fehlerfall deutlich
Document.png Durch das Erhöhen des Provelevels können unter Umstände manche Aussagen verifiziert werden, welche bei einem niedrigeren Level aufgrund eines Zeitfaktors fehlschlagen

Zeitaufteilung Scheduler Projekt

Der Abschnitt Zeitverteilung geht detaillierter darauf ein, wie sich die Projektaufwände verteilen.

  • Gesamtprojektaufwand kategorisiert gemäß Modulhandbuch
  • Verteilung der praktischen Aufwände (Migrationsaufwände, Verifikation, Projektkoordination und Simulationsentwicklung)
  • Gegenüberstellung Lines of Code: C und SPARK

[weiterlesen]

Erläuterungen zum SPARK Code

Dieses Kapitel soll eine Hilfestellung sein, um schnell in den entstandenen SPARK Code reinzufinden.

Neben einer Übersicht zu den verschiedenen SPARK Modulen, ist hier ebenfalls eine Erläuterung, wie die Listen aus dem C-Code nach SPARK migriert wurden.

[weiterlesen]

Simulation

Das am Projektende entwickelte Simulations Modul, erlaubt es die Funktionen des Schedulers zu erproben und zu visualieren.

[weiterlesen]

Offene Punkte des Projektes

Die Zeit hat leider nicht ausgereicht um alle zu Beginn gesetzten Ziele zu erreichen und darüberhinaus gibt es Stellen in dem entstanden SPARK Code, die einer Nacharbeit bedürfen.

Diese Punkte werden im verlinkten Abschnitt aufgeführt und jeweils kurz erläutert.

[weiterlesen]

Ausblick

Auf den Ergebnissen und Erkenntnissen aufbauend bieten sich folgende Folgeprojekte an:

  • Fortsetzen der bisherigen Arbeit und dabei die offenen Punkte schließen.
    Desweiteren könnte man sich in diesem Umfeld mit der Entwicklung einer domänenspezifischen Verifikationsbibliothek beschäftigen.
  • Neuer Migrationsversuch mit dem Fokus auf den Objektorientierungsmöglichkeiten von SPARK.