Efficient state space exploration of reactive object-oriented programs

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.

Level thesis:degree_level

thesis.doctoral

Grantor dc:publisher

Universität Oldenburg

Year

2005

Author dc:creator

• Lettrari, Marc

• [Keine Schlagwörter von Autor/in vergeben.]

Repository record source_url

http://oops.uni-oldenburg.de/82

OAI identifier oai:identifier

oai:oops.uni-oldenburg.de:82