Publikationen zum Fachbereich BDD

Publikationen in Zeitschriften und Büchern

• Kathrin Kaschner, Peter Massuthe, and Karsten Wolf. Symbolic Representation of Operating Guidelines for Services. Petri Net Newsletter, 72: 21-28, April 2007.

• Farn Wang, Karsten Schmidt, Fang Yu, Geng-Dian Huang, and Bow-Yaw Wang. BDD-Based Safety-Analysis of Concurrent Software with Pointer Data Structures Using Graph Automorphism Symmetry Reduction. IEEE Transactions on Software Engineering (TSE), 30(6): 403-417, June 2004.

  Abstract: Dynamic data-structures with pointer links, which are heavily used in real-world software, cause extremely difficult verification problems. Currently, there is no practical framework for the efficient verification of such software systems. We investigated symmetry reduction techniques for the verification of software systems with C-like indirect reference chains like x->y->z->w. We formally defined the model of software with pointer data structures and developed symbolic algorithms to manipulate conditions and assignments with indirect reference chains using BDD technology. We relied on two techniques, inactive variable elimination and process-symmetry reduction in the data-structure configuration, to reduce time and memory complexity. We used binary permutation for efficiency, but we also identified the possibility of an anomaly of false image reachability. We implemented the techniques in tool Red 5.0 and compared performance with Murø and SMC against several benchmarks.

  

Konferenzbeiträge und Beiträge auf Workshops

• Kathrin Kaschner, Peter Massuthe, and Karsten Wolf. Symbolische Repräsentation von Bedienungsanleitungen für Services. In Daniel Moldt, editor, 13. Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN 2006), Proceedings, pages 54-61, September 2006. Universität Hamburg. Note: In German.

• Farn Wang and Karsten Schmidt. Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures. In Doron Peled and Moshe Y. Vardi, editors, Proc. Int. Conf. Formal Techniques for Networked and Distributed Systems (FORTE 2002), volume 2529 of Lecture Notes in Computer Science, pages 50-64, 2002. Springer-Verlag.

  Abstract: We formally define the model of software with pointer data structures. We developed symbolic algorithms for the manipulation of conditions and assignments with indirect operands for verification with BDD-like data-structures. We rely on two techniques, including inactive variable elimination and process-symmetry reduction in the data-structure configuration, to contain the time and memory complexity. We use binary permutation for efficiency but also identify the possibility of anomaly of image false reachability. We implemented the techniques in tool red and compare performance with Mur and SMC against several other benchmarks.

  

Studien- und Diplomarbeiten

• Kathrin Kaschner. BDD-basiertes Matching von Services. Diplomarbeit, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, March 2006.

  Abstract: Moderne Software-Systeme werden zunehmend nach dem Paradigma der ServiceorientiertenArchitektur (SOA) aus unabhängigen Services zusammengesetzt, die definierte Funktionen zur Verfügung stellen und Nachrichten miteinander austauschen. Eine Möglichkeit zur Gewährleistung der reibungslosen Kommunikation besteht in der Bereitstellung einer Bedienungsanleitung durch den Service Provider, mit der der Service Broker anhand eines Prüfverfahrens - dem Matching - entscheiden kann, ob der Service eines Service Requesters zu dem angebotenen Service passt. Für die praktische Anwendung müssen Bedienungsanleitungen in geeigneter Weise kodiert werden. In der vorliegenden Arbeit werden dazu Binäre Entscheidungsdiagramme (BDDs) genutzt. Für das Matching wird der Service des Service Requesters durch einen Serviceautomaten modelliert, der seinerseits ebenfalls in eine BDD-Darstellung überführt wird. Darauf aufbauend wird schließlich ein Matching-Algorithmus entwickelt und seine Korrektheit bewiesen. Die Effizienz der Kodierung durch BDDs und die Funktionsweise des BDD-basierten Matching-Algorithmus wird an Beispielen gezeigt.

  

• Kathrin Kaschner. Repräsentation von Bedienungsanleitungen durch BDDs. Studienarbeit, Humboldt-Universität zu Berlin, January 2006.

zurück zur Übersicht