Eine aus Anforderungen bestehende Spezifikation stellt die Grundlage für Entwicklungsprojekte dar. Fehler, die in der Spezifikation enthalten sind, wirken sich auf den gesamten Entwicklungsprozess aus. Im schlimmsten Fall pflanzen sie sich durch den Entwicklungs- und Testprozess fort und werden erst beim Abnahmetest entdeckt. Die Vermeidung von Fehlern in Spezifikationen ist daher eine Grundvoraussetzung für eine zügige und kostengünstige Entwicklung. Handelt es sich um sicherheitskritische Systeme, dann können Fehler in der Spezifikation im Ernstfall Menschenleben gefährden oder großen finanziellen Schaden nach sich ziehen. Eine Überprüfung der Spezifikationen sollte daher nicht nur manuell, sondern auch formal sowie vollständig und so weit wie möglich automatisiert durchgeführt werden. Die immer stärkere Verbreitung von Produktlinien, die sich durch die Strukturierung von Variabilität und Gemeinsamkeiten verwandter Produkte mit dem Ziel der Wiederverwendung auszeichnen, steigert die Komplexität der Überprüfung der Spezifikationen im Entwicklungsprozess. Durch die Vielzahl von Produkten, die aus einer Produktlinie abgeleitet werden können, ist eine manuelle Überprüfung der Spezifikation kaum noch möglich. Handelt es sich um Spezifikationen eingebetteter Systeme, so wird die Überprüfung durch die Aufteilung in Soft- und Hardware weiter erschwert. Im Rahmen dieser Dissertation wird ein Verfahren vorgestellt, das Spezifikationen auf Widersprüche, Vollständigkeit und Redundanz überprüft. Dieses Verfahren ist sowohl für Spezifikationen einzelner Produkte also auch für solche, die Gemeinsamkeiten und Unterschiede von Produktlinien beschreiben, einsetzbar. Die Analyse der Spezifikationen basiert auf bekannten Algorithmen aus der formalen Verifikation von Hardwareschaltungen. Eine Anwendung dieser Algorithmen für Verhaltensbeschreibungen verschiedener Systeme sowie die Erweiterung durch Variabilität wird erläutert. Weiterhin wird auf die Generierung von „Orakeln“ eingegangen, die sich für die Voraussage von Testergebnissen eignen und ebenfalls auf Algorithmen aus der formalen Verifikation von Hardwareschaltungen basieren. Außerdem können auf einem „Orakel“ Annahmen über das Systemverhalten bewiesen werden. Zusätzlich wird ein Modell für die strukturierte Darstellung von Testfällen eingeführt. Die Testfälle können auf dem „Orakel“, einem weiteren Systemmodell oder auf dem System selbst ausgeführt werden. Die in dieser Dissertation vorgestellten Konzepte wurden an Beispielen aus dem universitären und dem industriellen Umfeld erprobt.