Formale Methoden

Formal Methods Application: An Empirical Tale of Software Development

  • Motivation: nützen formale Methoden?
  • Studenten von Miama University, pro Gruppe Aufteilung in Teams (6 formale Methode, 13 Kontroll), ver. Lehrpläne
  • Aufgabe: Entwicklung eines Aufzugsystems (Problem aus IEEE Workshop)
  • freiweilige Abgabe von Quellcode, UML, Pseudoalgorithmen
  • keine angegebenen Hypothesen
  • Ergebnisse
    • Kontrollgruppe: kein UML, Pseudoalgorithmen "schlecht", nur 5 nach Tests, keine Dokumentation
    • Testgruppe: 3x UML, 4x Spezifikation, alle 6 nach Tests, etwas Dokumentation
    • Vergleich: OO-Entwurf ähnlich, Algorithmen Testgruppe effizienter, Testgruppe besser implementiert, keine statistische Varianz (außer α=0.2\alpha = 0.2, Ausreißer entfernen), besserer Stil der Testgruppe
    • Vergleich Studenten (4 aus Testgruppe, außerhalb des Rahmens) vs IEEE Workshop: stud. Lösung detailierter
  • Gültigkeitsbedrohungen
    • Experimentdesign: freiwillige Zuteilung, Differenzen: Motivation, Kontakt, Lernstil, Skill
    • Hawthorne Effekt: Subjekte haben gewusst sie sind in einem Expirement
    • Novelty Effekt: Verschiedene Reaktion des Subjekts, wenn etwas neues gemacht wird
    • Subjekte versuchen Erwartungen des Experimentierers gerecht zu werden
    • Unbeherrschtheit: keine Kontrolle der Kontrollgruppe (wahrs. Code & Fix)
    • Quasi-Experiment --> kein kausaler Zsh. feststellbar
    • Test: nur 6 Testfälle --> zufällige Tests, Goldprogramm
    • Weglassen von Informationen: kontrahierendes Paper nicht referenziert, ...
    • intern: biased (wollen emp. Beweis), Co-Autor ist Student
    • schwammige Anforderungen --> Ergebnisse nicht vergleichbar
    • Metriken: Prägnanz in LOC?, Komplexität: #Loops, max Nesting?, Stil qualitativ?

Two controlled Experiments concerining the Usefulness of Assertions as a Means for Programming

  • Ausgangspunkt: Meyer's Hypothesen (Programmkorrektheit + Programmverständnis, fehlend: Dokumentation + Testen)
  • Hypothesen: Zuverlässigkeit + Aufwand
  • gemeinsam: Studenten (PSP Kurs), zwingende Teilnahme, Fragebogen
  • Experiment 1: gegenbalanciert, 9 Teilnehmer (Einteilung: PSP-Kurs Produktivität), 2 unabh. Aufgaben (in C, 1 unabh. vom restlichen Code (String), 1 abh. (Chain)), vorheriger Webkurs
  • Experiment 2: single-factor post-test only inter-subject, 13 Teilnehmer (6 Kontrollgruppe), Aufgabe: Graphbase vervollständigen, 3 Phasen: Webkurs, Implementierung, Korrektur (EG: Nachbedingungen, KG: natürliche Sprache)
  • Ergebnisse
    • gemeinsam: geringe Güte (0,41 bzw. 0,52), alle nicht stat. relevant
    • Experiment 1: Arbeitszeit (nur nach Anpassung p = 0.06 für H2), Wiederverwendung (Chain + reuse in assert, p = 0.07)
    • Experiment 2: Arbeitszeit irrelevant, Wiederverwendung irrelevant, Verlässlichkeit (H1 nur nach IP)
    • Wartungsaufwand, Wiederverwendung: EXP1 != EXP2
    • Aufwand+ falls unabh. von restlichem Code
  • Gültigkeitsbedrohungen
    • intern: Historie (2 Monate), wenige Teilnehmer
    • extern: Studenten, geringe Einarbeitungszeit / Vertrautheit

Investigating the Influence of Formal Methods

  • Fallstudie über Entwicklung eines Luftverkehrskontrollinformationssyste, 200k LOC
  • Spezifikation: Formal (10 VDM, 1 FSM, 2 VDM + CCS), Informal (4 Pseudocode)
  • 3000 Fehler während Entwicklung (2 Jahre), 148 nach Inbetriebnahme (nur Kategorie > 0),
  • Betrachtung: Auswirkungen von Fehlern (#Module)
  • Ergebnisse
    • keine stat. relevanten Beweise: Kosteneffizienz, Verlässlichkeit, ausreichendes Training
    • evtl. ("Nebenprodukte"): Entwickler- --> Fehler-,
    • Codeänderungen irrelevant, leichter testbar
    • alleine kein Qualität+, Unit Test --> Error-, nach Lieferung Fehler-
    • Fazit: Formale Methoden = Katalysator