Lettrari, Marc (2006) Efficient state space exploration of reactive object-oriented programs. PhD, Universität Oldenburg.

Preview

Volltext (1692Kb)

Abstract

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.

["eprint_fieldname_abstract_plus" not defined]

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.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	[Keine Schlagwörter von Autor/in vergeben.]
Controlled Keywords:	Eingebettete Programme, Zustandsexploration
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law
Date Deposited:	17 Jan 2013 14:13
Last Modified:	17 Jan 2013 14:13
URI:	https://oops.uni-oldenburg.de/id/eprint/82
URN:	urn:nbn:de:gbv:715-oops-1125
DOI:
Nutzungslizenz:

Actions (login required)

View Item