In dieser Arbeit werden neue Ansätze zur Zustandsexploration von eingebetteten C++ Programmen vorgestellt, die eine effiziente Suche nach Zuständen mit bestimmten Eigenschaften erlauben. Um eine einheitliche Behandlung von eingebetteten C++ Programmen zu ermöglichen, wird zunächst eine Erweiterung SymC++ von C++ um die Konzepte Parallelität und Synchronisation vorgestellt. Der erste vorgestellte Ansatz zur Zustandsexploration beruht auf einer kombinierten explizit-symbolischen Darstellung von Zustandsmengen von SymC++ Programmen, die eine kompakte Repräsentation von großen Zustandsmengen und eine effiziente Realisierung von Operationen auf diesen Zustandsmengen ermöglicht. Der zweite Ansatz beruht auf der Anwendung heuristischer Suchmethoden in der Zustandsexploration. Wir entwickeln einen neuen Ansatz zur heuristischen Zustandsexploration auf der Basis automatisch generierter Abstraktionen der zu untersuchenden Programme. Die vorgestellten Ansätze werden implementiert und experimentell evaluiert. <dt.>
In this thesis we present new approaches for state space exploration of embedded C++ programs that allow an efficient search towards program states with specific properties. To facilitate a uniform treatment of embedded C++ programs, we define the language SymC++ that extends C++ with the concepts of concurrency and synchronization. The first presented approach to state space exploration is based upon a composite explicit-symbolic representation of sets of states of SymC++ programs that allows a compact treatment of large sets of states and an efficient realization of operations on sets of states. The second approach employs heuristic search methods for state space exploration. We develop a new approach for heuristic state space exploration that is based upon automatically generated abstractions of the considered programs. The presented approaches have been implemented and evaluated experimentally. <engl.>
