Um die Qualität von Software zu verbessern und zertifizierbar zu machen, werden vor allem im Bereich sicherheitskritischer Anwendungen (safety und security) formale Techniken zum Testen und zur Verifikation verwendet.

Wir beschäftigen uns mit Techniken zum automatisierten, systematischen Test von objektorientierten und eigebetteten Systemen. Grundlage dafür bilden mathematisch fundierte Modelle, die zum Einem für die Ableitung von Testfällen herangezogen werden und zum Anderen für eine qualitative Beurteilung der Testdurchfuührung benutzt werden.

Zur Validierung von Softwaremodellen wird die Erweiterung der Anwendbarkeit von Modellprüfungstechniken und Beweisverfahren durch geeignete Abstraktionsverfahren betrachtet. Auch im Bereich der Sicherheit in verteilten Rechnernetzen haben Modellprüfungstechniken, z.B. zur Analyse von Authentifikationsprotokollen, Anerkennung gefunden.

Schließlich erlauben interaktive Theorembeweiser die formale Modellierung und mechanische Verfikation von Systemen und ihrer Eigenschaften. Hier sind seit neuestem große Fortschritte bei der Verifikation von Sicherheitseigenschaften von Programmiersprachen und Systemen zu verzeichnen. Z.B. ist Java und seine Virtual Machine vollständig in Isabelle/HOL eingebettet und bezüglich klassischer Typsicherheit analysiert.

Genauer forschen wir gegenwärtig in der Gruppe SWT auf folgenden Gebieten:

1. Automatische Testfallgenerierung aus formalen Spezifikationen
2. Semantische Fundierung von zustandsbasierten Systemmodellen (Statecharts und State Machines)
3. Eigenschaftserhaltene Abstraktionstechniken und Modellchecking für zustandsbasierte Systemmodelle
4. Mechanisch gestützte Beweise von Sicherheitseigenschaften, z.B. Non-Interference, der JVM
5. Einsatz von interaktiver Beweistechnik für die Fundierung und Analyse neuer Paradigmen, wie Aspekte und Kollaborationen