Filtern
Erscheinungsjahr
- 2002 (5) (entfernen)
Schlagworte
- OBDD (2)
- OBDDs (2)
- Algorithmus (1)
- Datenstruktur (1)
- Distributed Systems (1)
- Erweiterung (1)
- Formal Verification (1)
- Hyperlink-Management (1)
- Integrated Circuits (1)
- Logischer Entwurf (1)
Institut
- Informatik (5) (entfernen)
Insbesondere im wissenschaftlichen Bereich ist es zur Selbstverständlichkeit geworden, zur Befriedigung eines Informationsbedürfnisses zunächst das World Wide Web (Web) zu benutzen. Der komplexe Aufbau des Webs und die dort herrschende Unordnung machen das Auffinden bestimmter Dokumente zu einem diffizilen Vorgang. Suchmaschinen und Web-Verzeichnisse unterstützen den Benutzer hierbei; ihre effektive Nutzung ist jedoch nicht einfach. Es ist daher hilfreich, Suchdienste zu entwickeln, welche Kontextwissen mitbringen. In der vorliegenden Arbeit wird das Verfahren der thematisch spezialisierten Suche präsentiert und anhand der Menge der persönlicher Home Pages von Informatikern exemplifiziert. Der Bibliographie-Server DBLP.uni-trier.de liefert u.a. zu über 4.000 Wissenschaftlern manuell gesammelte persönliche Home Pages. Durch verschiedene Analysen werden in dieser Menge häufig vorkommende, also relevante Eigenschaften ermittelt. Dies ist ein kreativer Prozess, in den sowohl Suchwissen -- Wissen über Techniken des Suchens im Web -- als auch Fachwissen -- Wissen über die Beschaffenheit persönlicher Home Pages -- einfließen. Nach der Überprüfung dieser Eigenschaften auf ihre Signifikanz in der Gesamtheit der Web-Dokumente ist ein thematisch spezialisiertes Wissen erschaffen worden. Zur Durchführung der Suche würde man idealerweise alle Web-Dokumente mit Hilfe des erarbeiteten Wissens und des Anfrageterms -- des vollständigen Namens eines Informatikers -- untersuchen. Da das Web aus mehreren Milliarden Dokumenten besteht, ist dies praktisch nicht durchführbar: Es ist notwendig, eine geeignete Vorauswahl zu treffen. Suchmaschinen haben Daten zu vielen Web-Dokumenten erfasst. Deshalb wird mit ihrer Hilfe unter Verwendung des Anfrageterms eine Vorauswahl getroffen. Um nun die Dokumente der Vorauswahlmenge gemäß der Anfrage zu bewerten wird das thematisch spezialisierte Wissen adäquat in einer Bewertungsfunktion repräsentiert, welche jedem Dokument einen Wert zuweist und somit eine Rangfolge erstellt. Das Design der Bewertungsfunktion ist eine schöpferische Tätigkeit: Die sachgerechte Gewichtung der verschiedenen Eigenschaften bestimmt maßgeblich das Gelingen des Verfahrens. Der vornehmlich in Java implementierte, vollautomatisierte Web-Dienst HomePageSearch (hpsearch.uni-trier.de) führt regelmäßig für über 100.000 Namen diesen Suchvorgang durch. Der Benutzer kann auf das in einer DB2-Datenbank gespeicherte Ergebnis zurückgreifen. Durch die periodische Neuberechnung des thematisch spezialisierten Wissens wird der Dynamik des Webs Rechnung getragen. Der modulare und stark parametrisierte Aufbau des Systems erleichtert die Portierung des Verfahrens auf andere Mengen von Web-Dokumenten. Nicht zuletzt aufgrund der starken Verlinkung mit DBLP und ResearchIndex wird HomePageSearch von vielen Wissenschaftlern intensiv genutzt.
Hardware bugs can be extremely expensive, financially. Because microprocessors and integrated circuits have become omnipresent in our daily live and also because of their continously growing complexity, research is driven towards methods and tools that are supposed to provide higher reliability of hardware designs and their implementations. Over the last decade Ordered Binary Decision Diagrams (OBDDs) have been well proven to serve as a data structure for the representation of combinatorial or sequential circuits. Their conciseness and their efficient algorithmic properties are responsible for their huge success in formal verification. But, due to Shannon's counting argument, OBDDs can not always guarantee the concise representation of a given design. In this thesis, Parity Ordered Binary Decision Diagrams are presented, which are a true extension of OBDDs. In addition to the regular branching nodes of an OBDD, functional nodes representing a parity operation are integrated into the data structure, thus resulting in Parity-OBDDs. Parity-OBDDs are more powerful than OBDDs are, but, they are no longer a canonical representation. Besides theoretical aspects of Parity-OBDDs, algorithms for their efficient manipulation are the main focus of this thesis. Furthermore, an analysis on the factors that influence the Parity-OBDD representation size gives way for the development of heuristic algorithms for their minimization. The results of these analyses as well as the efficiency of the data structure are also supported by experiments. Finally, the algorithmic concept of Parity-OBDDs is extended to Mod-p-Decision Diagrams (Mod-p-DDs) for the representation of functions that are defined over an arbitrary finite domain.
Mobile computing poses different requirements on middleware than more traditional desktop systems interconnected by fixed networks. Not only the characteristics of mobile network technologies as for example lower bandwidth and unreliability demand for customized support. Moreover, the devices employed in mobile settings usually are less powerful than their desktop counterparts. Slow processors, a fairly limited amount of memory, and smaller displays are typical properties of mobile equipment, again requiring special treatment. Furthermore, user mobility results in additional requirements on appropriate middleware support. As opposed to the quite static environments dominating the world of desktop computing, dynamic aspects gain more importance. Suitable strategies and techniques for exploring the environment e.g. in order to discover services available locally are only one example. Managing resources in a fault-tolerant manner, reducing the impact ill-behaved clients have on system stability define yet another exemplary prerequisite. Most state of the art middleware has been designed for use in the realm of static, resource rich environments and hence is not immediately applicable in mobile settings as set forth above. The work described throughout this thesis aims at investigating the suitability of different middleware technologies with regard to application design, development, and deployment in the context of mobile networks. Mostly based upon prototypes, shortcomings of those technologies are identified and possible solutions are proposed and evaluated where appropriate. Besides tailoring middleware to specific communication and device characteristics, the cellular structure of current mobile networks may and shall be exploited in favor of more scalable and robust systems. Hence, an additional topic considered within this thesis is to point out and investigate suitable approaches permitting to benefit from such cellular infrastructures. In particular, a system architecture for the development of applications in the context of mobile networks will be proposed. An evaluation of this architecture employing mobile agents as flexible, network-side representatives for mobile terminals is performed, again based upon a prototype application. In summary, this thesis aims at providing several complementary approaches regarding middleware support tailored for mobile, cellular networks, a field considered to be of rising importance in a world where mobile communication and particularly data services emerge rapidly, augmenting the globally interconnecting, wired Internet.
Today, usage of complex circuit designs in computers, in multimedia applications and communication devices is widespread and still increasing. At the same time, due to Moore's Law we do not expect to see an end in the growth of the complexity of digital circuits. The decreasing ability of common validation techniques -- like simulation -- to assure correctness of a circuit design enlarges the need for formal verification techniques. Formal verification delivers a mathematical proof that a given implementation of a design fulfills its specification. One of the basic and during the last years widely used data structure in formal verification are the so called Ordered Binary Decision Diagrams (OBDDs) introduced by R. Bryant in 1986. The topic of this thesis is integration of structural high-level information in the OBDD-based formal verification of sequential systems. This work consist of three major parts, covering different layers of formal verification applications: At the application layer, an assertion checking methodology, integrated in the verification flow of the high-level design and verification tool Protocol Compiler is presented. At the algorithmic layer, new approaches for partitioning of transition relations of complex finite state machines, that significantly improve the performance of OBDD-based sequential verification are introduced. Finally, at the data structure level, dynamic variable reordering techniques that drastically reduce the time required for reordering without a trade-off in OBDD-size are described. Overall, this work demonstrates how a tighter integration of applications by using structural information can significantly improve the efficiency of formal verification applications in an industrial setting.
Die eigene Web-Präsenz hat sich für Unternehmen zu einem nicht mehr wegzudenkenden Instrument, einer flexiblen Schnittstelle zum Kunden, entwickelt. Mit ihr wird eine global erreichbare Anlaufstelle offeriert: Die Chancen der Online-Techniken nutzend ist dem Unternehmen mit seiner Web-Präsenz ein Medium für die "klassische" Werbung, darüber hinaus ein Direkt-Marketing- und Dialog-Medium sowie weiterhin ein eigenes Marktforschungs-Instrument an die Hand gegeben. Dessen Entwicklung und speziell sein Betrieb stellen für ein Unternehmen in verschiedenen Hinsichten eine ernstzunehmende Herausforderung dar. Aus organisatorischer Sicht ist hier die nicht einfach zu realisierende Integration der Web-Präsenz in das Unternehmen anzustreben: Nicht einem isoliert arbeitenden, technikverliebten Mitarbeiter, dem "`Webmaster"', obliegt die Pflege der Web-Präsenz als Allein-Zuständigen, sondern entsprechend ihren Zuständigkeiten übernehmen anteilig die in den Fachabteilungen des Unternehmens tätigen Arbeitskräfte diese Aufgabe. Aus technischer Sicht stellt eine moderne Web-Präsenz ein umfangreiches, und bei hoher Dynamik entsprechend komplexes Produkt dar, für dessen Realisierung nicht unerhebliche Anstrengungen unternommen werden müssen -- insbesondere dann, wenn die zugrundeliegende Technik den organisatorischen Anforderungen innerhalb des Unternehmens gerecht werden soll. Bedingt durch die hohe Innovationsrate im Umfeld der Internet-Technologie befinden sich die Anforderungen an die Betreiber einer Web-Präsenz in einem steten Wandel und erschweren damit den Unternehmen den Einstieg in dieses Medium. Gerade die in vielen Fällen in den Unternehmen noch eingesetzten proprietären Lösungen erfordern aus technischer Sicht einen hohen Integrationsaufwand, wenn die darin vorgehaltenen Informationen für die Web-Präsenz automatisiert einer Zweitverwendung zugeführt werden sollen. Über die zusätzliche Nutzung der Unternehmens-Web-Präsenz bzw. des Systems, mit dem sie erstellt und verwaltet wird, für die unternehmensinterne Arbeit, d.h. für das Intranet, kann der für das Unternehmen entstehende Aufwand relativiert werden. In das Bild des Lebenszyklus' einer modernen Web-Präsenz eingebettet, steht die Konzeption und Entwicklung eines an die im Umfeld des Web-Präsenz-Managements in Unternehmen vorzufindenden Randbedingungen flexibel anpassbaren Online-Redaktionssystems im Vordergrund dieser Arbeit. Zentraler Bestandteil seiner Konzeption ist die Idee, ein sich aus derart vielen separaten Elementen zusammensetzendes, komplexes Gesamtdokument wie eine Unternehmens-Web-Präsenz durch eine wachsende Mitarbeiterzahl -- direkt von deren jeweiligen Arbeitsplätzen aus -- gemeinsam aufzubauen und zu pflegen. Der Praxiseinsatz des bedarfsgerecht in seinen endgültigen Ausprägungen auf die speziellen Belange der Unternehmen maßgeschneiderten Systems begründet die konsequente Nutzung von Internet-Technologien sowie die auf offenen Standards basierende Implementation durch flexible plattformunabhängige Installation und einfache Integration. Im Anschluss an ein einleitendes Kapitel beschreibt diese Arbeit ausgehend von der Problemstellung sowie technischen Grundlagen die Konzeption, Implementation und den Einsatz des webbasierten Online-Redaktionssystems bevor eine Einordnung und schließlich die Zusammenfassung den Abschluss dieser Arbeit bilden.