Veröffentlichung zur European Joint Conferences on Theory and Practice of Software (ETAPS), 7th Workshop on Model-Based Testing in Tallin.

Abstract: Test generation and test data selection are difficult tasks for model based testing. Tests for a program can be meld to a test suite. A lot of research is done to quantify the quality and improve a test suite. Code coverage metrics estimate the quality of a test suite. This quality is fine, if the code coverage value is high or 100%. Unfortunately it might be impossible to achieve 100% code coverage because of dead code for example. There is a gap between the feasible and theoretical maximal possible code coverage value. Our review of the research indicates, none of current research %done in testing is concerned with exact gap computation. This paper presents a framework to compute such gaps exactly in an ISO-C compatible semantic and similar languages. We describe an efficient approximation of the gap in all the other cases. Thus, a tester can decide if more tests might be able or necessary to achieve better coverage.

Download: mbt12.pdf

Veröffentlichung bei der Konferenz Software Engineering 2012 für die Arbeitstagung Programmiersprachen (ATPS'12) in Berlin.

Abstract: Viele Aussagen zum Programmverhalten sind in turingmächtigen Programmiersprachen unentscheidbar (Rice Theorem). Mittels Abstraktion vom Programmverhalten können nicht-turingmächtige Modelle automatisch erzeugt werden. Modelle in Form von symbolischen Kellersystemen (SPDS) erlauben eine so präzise Darstellung des Programmverhaltens, so dass eine ISO-C konforme Semantik möglich ist. Allerdings führen präzisere Darstellungen auch zu komplexeren und umfangreicheren Modellen. Dies erschwert Software-Modellprüfung, modellbasiertes Testen und Testdaten- und Codegenerierung. Mehr Abstraktion führt hingegen zu kleineren Modellen, allerdings auch zu mehr Fehlalarmen. Ziel dieser Arbeit ist es, bezüglich temporaler Aussagen unwichtige Teile eines SPDS zu identifizieren und von diesen Teilen so zu abstrahieren, dass keine Fehlalarme entstehen.

Download: atps12.pdf

Dissertation "Programmanalysen zur Verbesserung der Softwaremodellprüfung".

Abstract: Die Softwarequalität kann mittels Modellprüfung gesteigert werden, indem formale Eigenschaften von Software bzw. davon abgeleitete Modelle verifiziert werden. Die derzeit verfügbaren Modellprüfer sind nicht in der Lage, Quelltexte komplexer Softwareprojekte selbständig, automatisiert und ohne Fehlalarme zu überprüfen. Um Fehlalarme zu reduzieren, wurden präzise Modelle in Form von symbolischen Kellersystemen (SPDS) betrachtet und Verfahren entwickelt, welche die Softwaremodellprüfung verbessern. Da Modellprüfer sehr sensitiv auf die Größe des betrachteten Zustandsraumes reagieren, wurden vorrangig Techniken zu seiner Verkleinerung entworfen, ohne den Wahrheitsgehalt der zu prüfenden Eigenschaften zu verändern. Neben neuen theoretischen Erkenntnissen wurde experimentell gezeigt, dass so in einigen Fällen die Modellprüfung erst ermöglicht wird und in anderen Fällen sich die Modellprüfung sogar ganz erübrigt.

Download: diss.pdf

Anlagen: diss.zip

Veröffentlichung im Rahmen des 16. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'11) auf Schloss Raesfeld.

Abstract: Zur Software-Modell-Prüfung, zum modellbasierten Testen und bei der Testdaten- und Codegenerierung sind die Größe und Komplexität von Modellen entscheidende Einflussfaktoren. Aus Quellcode (z.B. C oder Java) gewonnene Modelle in Form von symbolischen Kellersystemen (SPDS) erlauben nicht nur präzisere Ergebnisse, sondern führen auch ohne Modellexplosion bei exakter Nachbildung von Rekursion zu weniger Fehlalarmen als die Modellprüfung endlicher Systeme. Derart gewonnene Modelle beschreiben allerdings viel unwichtiges Verhalten sehr detailliert, was den Zustandsraum unnötig vergrößert und damit Modell-Prüfung, Testen usw. erschwert. Eine Form zur Vermeidung dieses unwichtigen Verhalten in der Modellbeschreibung ist die Abstraktion. Dabei wird das Programm oder komplexe Modell in ein weniger detailliertes Modell überführt. Ziel dieser Arbeit ist es, unwichtige Teile der Modellbeschreibung eines SPDS durch gegebene temporale Formeln selektiv zu identifizieren und davon zu abstrahieren.

Download: kps11.pdf

Veröffentlichung im Rahmen der "36th EUROMICRO Conference on Software Engineering and Advanced Applications", Lille, France, September 01-03.

Abstract: In several works a method was suggested to overcome the lack of signature-based composition currently enabled in component-based and service-oriented architectures (SOA). Several approaches allow to encode non-functional properties of a single component in a contract (component protocol) where the remote calls to a component are taken into consideration. Component protocols ensures that bugs or unsafe behavior caused interaction sequences are obeyed. Encoding business rules works fine as these contracts can be derived from human knowledge only and have to be defined manually, too. In this work we will show, how such unsafe behavior within source code can be discovered and prevented by automatic component protocol generation and model checking techniques..

Download: seaa2010.pdf

IEEE doi: http://doi.ieeecomputersociety.org/10.1109/SEAA.2010.30

Veröffentlichung im Rahmen der "Sixth International Conference on Algorithmic Aspects in Information and Management", July 19 - 21, 2010, Shandong University, Weihai, China.

Abstract: This paper presents an iterative, highly parallelizable approach to find good tours for very large instances of the Euclidian version of the well-known Traveling Salesman Problem (TSP). The basic idea of the approach consists of iteratively transforming the TSP instance to another one with smaller size by contracting pseudo backbone edges. The iteration is stopped, if the new TSP instance is small enough for directly applying an exact algorithm or an efficient TSP heuristic. The pseudo backbone edges of each iteration are computed by a window based technique in which the TSP instance is tiled in non-disjoint sub-instances. For each of these sub-instances a good tour is computed, independently of the other sub-instances.  An edge which is contained in the computed tour of every sub-instance (of the current iteration) containing this edge is denoted to be a pseudo backbone edge. Paths of pseudo-backbone edges are contracted to single edges which are fixed during the subsequent process.

Download: aaim2010.pdf

Veröffentlichung im Rahmen des 15. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'09) in Maria Taferl.

Abstract: Often, it is argued that some problems in data-flow analysis such as e.g. worst case execution time analysis are undecidable (because the halting problem is) and therefore only a conservative approximation of the desired information is possible. In this paper, we show that the semantics for some important real programming languages - in particular those used for programming embedded devices - can be modeled as finite state systems or pushdown machines. This implies that the halting problem becomes decidable and therefore invalidates popular arguments for using conservative analysis.

Download: kps09z.pdf

Veröffentlichung im Rahmen des 15. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'09) in Maria Taferl.

Abstract: Intervallanalysen bestimmen zu einem gegebenen Programm konservative oder nicht-konservative Wertebereiche von Variablen. Desto genauer diese Wertebereiche bestimmt werden können, desto präziser sind die darauf basierenden Analysen wie z.B. die Laufzeitschätzung von Programmen bzw. führen zu weniger Fehlalarmen wie z.B. bei der Prüfung auf Feldzugriffe außerhalb zulässiger Indizees (ArrayOutOfBounds). Bei unbeschränkter Rekursion und unbeschränktem Speicher (Heap/Halde) ist das Problem der Bestimmung von Wertebereichen maximaler Genauigkeit (auch als exakte Wertebereiche bezeichnet) unentscheidbar. Im Folgenden wird gezeigt, wie bei unbeschränkter Rekursion und beschränktem Speicher derartige exakte Wertebereiche in polynomieller Zeit (bzgl. Modellgröße) bestimmt werden können.

Download: kps09.pdf

Vortrag im Rahmen der 39. GI-Jahrestagung (Modellbasiertes Testen)

Download: motes09vortrag.pdf

Vortrag im 15. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'09).

Download: kps09vortrag.pdf