Weitere Themen

  1. Bezahlautomat / Geldwechsler (1 - 2 Themen)

    Es sind die Bezahlfunktion inkl. der Herausgeber von Wechselgeld bei Bezahlautomaten zu spezifizieren, zu implementieren und zu verifizieren.

    In einer Variante könnten auch Geldwechselautomaten betrachtet werden.

    Es sollte in jedem Fall auf eine möglichst generische Lösung geachtet werden.

  2. APDU-Tool: Operationen mit Bytearrays und Zeichenketten

    Bei der Programmierung von SmartCard-Applikationen sind Spezifikation und Implementierung der Kommunikation zwischen Lesegerät und SmartCard sicherheitskritisch und zugleich fehlerträchtig. Die Kommunikation erfolgt über Byte-Arrays.

    Als Minimum müssen Operationen für Byte-Arrays und deren Konversion in/aus andern Datentypen, z.B. Zeichenketten, spezifiziert, implementiert und verifiziert werden.

    evtl. tw. in KIV-Smart

  3. Flugzeug-Sicherheit: In [2] beschreibt Tim van Beveren Unfälle mit Flugzeugen, die ihre Ursache in fehlerhaften oder mißverstandenen Abbildungen der Steuerung von Flugzeugen beruhten.

    Es soll untersucht werden, ob durch formale Spezifikation und Validierung das Fehlverhalten haette aufgedeckt werden können.

    1. Teilprobleme, deren falsche oder mißverständliche Spezifikation, Implementierung und/oder Dokumentation zu Unfällen führten.

      1. Spoilerextension

      2. Fahrwerkausfahren

  4. Spezifikations-, Implementierungs und Verifikationsaufgaben im Zusammenhang mit Sicherheitswerkzeugen fuer das Internet.

  5. Spezifikations-, Implementierungs und Verifikationsaufgaben im Zusammenhang mit Konfigurationswerkzeugen fuer Betriebssysteme, z.B. der Konfiguration einer Firewall.

    Die Herausforderung besteht darin, Konfigurationswerkzeuge mit dem Anspruch auftreten, dem Anwender behilflich zu sein, ohne ihn mit der vollen Komplexität der zu konfigurierenden Mechanismen zu belasten. In der Praxis ist aber dem Anwender mitunter unklar, wie er die ihm überlassenen Entscheidungen treffen soll. Sind die Werkzeuge fehlerhaft? Ist der Anwender zu dumm? Stellen Konfigurationswerkzeuge einen Versuch der Quadratur des Kreises dar?

  6. Genotype - Phenotype:

    Es geht um die Spezifikation von ``Chromosomen'' und ``Individuen'' und von deren Zusammenhang im Sinne des Gene Expression Programming (GEP).

    Als Zusatzaufgabe oder in einem verbundenem Projekt könnte die Transformation vom Genotype in den Phenotype implementiert und verifiziert werden.

    Mehr Informationen: In [1]: In GEP (Gene Expression Programming) the individuals are encoded as linear strings of fixed length (the genome or chromosomes) which are afterwards expressed as nonlinear entities of different sizes and shapes (i.e., simple diagram representations or expression trees).

    http://www.gene-expression-programming.com

Uwe Petermann 2006-06-13