Da eingebettete Systeme immer komplexer werden, wird die Notwendigkeit einer genaueren Spezifikationen für Hardware und Software größer. Eine Möglichkeit ist die Benutzung von formalen Methoden. Model Checking ist eine bekannte, vollautomatische Methode für die formale Verifikation. Die Benutzung von BDDs (Symbolic Model Checking) erlaubt hier eine Verbesserung.
Die Verifikation wird durchgeführt, nachdem die Partitionierung ausgeführt wurde, obwohl die Eigenschaften sich auf die noch nicht partitionierten Systeme beziehen. Aus diesem Grund ist es nötig, diese Eigenschaften auch zu partitionieren, um sie modular verifizieren zu können. Außerdem benötigt die modulare Verifikation Hypothesen über die Module. Diese Hypothesen können durch ein automatisches model-checking-ähnliches Verfahren extrahiert werden. Ziel dieser Arbeit ist es zu bestimmen, wie Model Checking benutzt werden kann, um eingebettete Systeme zu verifizieren.