Vortragsprogramm - 06. November 2008

Modellbasiertes Testen elektronischer
Gesundheitskarten und Heilberufsausweise mittels asynchroner Produktautomaten

Dieser Beitrag beschreibt die Anwendung eines modellbasierten Verfahrens zur Testfolgengenerierung auf die deutschen elektronischen Gesundheitskarten, Heilberufsausweise und Sicherheitsmodulkarten, um deren Interoperabilität und Robustheit zu testen. Zur Modellierung der Chipkartenanwendungen werden asynchrone Produktautomaten (APA) verwendet.
Aus einem solchen operationalen Modell wird mittels des SH Verification Tool das dynamische Systemverhalten in Form eines Erreichbarkeitsgraphen berechnet. Dieser Graph wird dann entlang einer Chinese Postman Tour durchlaufen, um Kommandofolgen und die zu erwartenden Antwortfolgen zu ermitteln. Das verwendete Verfahren hat den Vorteil, dass damit komplexe Chipkartenanwendungen in kompakter und übersichtlicher Weise modelliert und automatisiert Testfolgen mit hoher Testabdeckung erzeugt werden können.