Das entscheidende Problem des Testens als Validierungstechnik besteht darin, dass es normalerweise das Vorhandensein von Fehlern zeigt, aber nicht deren Abwesenheit. 1975 zeigten Goodenough und Gerhart (GG), dass angemessen strukturierte Tests die Fehlerfreiheit eines Programms nachweisen können. Ihr Ansatz beinhaltet präzise Kriterien für die Auswahl von Testfällen. GG konzentrieren sich jedoch eher auf die Implementierung (Quellcode) eines Programms als auf seine Spezifikation als Modell, wodurch der Umfang ihres Ansatzes erheblich auf Programmcodes beschränkt wird.Der vorliegende Ansatz schlägt vor, das Konzept von GG auf die modellbasierte Analyse und das Testen sequentieller Systeme in toto (Hardware und Software) zu erweitern, basierend auf ihrer formalen Spezifikation, unter Verwendung der Konzepte des ganzheitlichen Testens und des Mutationstests, angereichert mit Erkenntnissen und Ergebnissen aus der Theorie der endlichen Automaten und regulären Ausdrücke.Ganzheitliches Testen umfasst in diesem Zusammenhang positives Testen, um zu zeigen, dass das getestete System so funktioniert, wie es der Benutzer wünscht, und negatives Testen, um zu zeigen, das getestete System nichts tut, was der Benutzer nicht wünscht. Techniken von Mutationstests werden verwendet, um den das getestete System so zu modifizieren, dass seine fehlerhaften Versionen generiert werden, um unerwünschte Situationen zu modellierenç Somit ermöglicht uns das vorgeschlagene modellbasierte ideale Testen (MBIT), sowohl das Vorhandensein als auch das Abwesenheit der Fehler im Rahmen der Spezifikation des getesteten Systems zu zeigen. Der Ansatz ist aufgrund der theoretischen Merkmale der verwendeten Techniken auf sequentielle Systeme beschränkt und wurde anhand verschiedener Fallstudien analytisch und experimentell demonstriert und bewertet: Verkehrsampel, grafische...

The crucial problem of testing as a validation technique is that it usually shows the presence of faults but not their absence. In 1975, Goodenough and Gerhart (GG) showed that adequately structured tests could demonstrate the absence of errors in a program. The phrase properly entails precisely defined criteria for selecting test cases. However, GG focus on the implementation (source code) of a program rather than its specification as a model, thus considerably limiting the scope of their approach to program codes only. The present approach proposes to extend GGs concept to model-based analysis and testing sequential systems in toto (hardware and software), based on their formal specification, using the concepts of holistic testing and mutation testing, enriched with knowledge and results from the theory of finite state machines and regular expressions. Holistic testing, in this context, comprises positive testing to show that the system under test functions the way the user desires and negative testing to show that the system under test does not do anything the user would not desire. On the other hand, mutation testing can be used to modify the system under test to generate its faulty versions to model undesirable situations to be checked against the corresponding implementation when the mutant system under test fails. Thus, the proposed model-based ideal testing (MBIT) enables us to show both the presence and the absence of the faults in the scope of the specification of the system under test.The approach is limited to sequential systems because of the theoretical features of the techniques used. These techniques are demonstrated and evaluated analytically and experimentally in various case studies: traffic light controllers, graphical user interfaces, and sequential circuits. The results will be critically discussed concerning the advantages and shortcomings ...