Im Entwurf und Test von elektronischen Systemen stellt sich die Aufgabe, Testmuster mit Anforderungsbeschreibungen abzugleichen. Dieser Artikel stellt eine Methodik zur formalen Verifikation von Testmustern bzgl. funktionalen, zeitannotierten Anforderungsbeschreibungen vor. Während Teile der Anforderungsbeschreibungen in temporallogische Formeln abgebildet werden können, liefern die Testfälle der Klassifikationsbaummethode das zustandsorientierte Modell, das verifiziert werden kann. Details dieses Verfahrens erläuterten wir anhand des Tests eines Tempomaten aus dem Automobilbau. Erste Ergebnisse zeigen, dass die Methodik selbst für große Testsequenzen anwendbar ist.
Modelchecking von Klassifikationsbaum-Testsequenzen
2005
10 Seiten, 7 Bilder, 9 Quellen
Conference paper
German