|
Geschrieben von: Dirk Richter
|
|
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 |
|
Geschrieben von: Dirk Richter
|
|
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
|
|
|
Geschrieben von: Dirk Richter
|
|
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 |
|
Geschrieben von: Dirk Richter
|
|
Veröffentlichung im Rahmen der 39. GI-Jahrestagung (Modellbasiertes Testen)
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. Für diese SPDS wurde ein Ansatz verfolgt, der die innere Struktur der Zustände ausnutzt, um den Zustandsraum der Modelle weiter zu verkleinern. Experimente zeigen, dass damit die Modellprüfung beschleunigt bzw. die Modellprüfung erst ermöglicht wird oder sich erübrigt.
Download: motes09.pdf
Quelle: GI-Edition Lecture Notes in Informatics (LNI), Modellbasiertes Testen im Rahmen der 39. GI-Jahrestagung.
Copyrightinhaber: Gesellschaft für Informatik |
|
|
|
|
|
Seite 1 von 2 |
Veröffentlichungen 
