SciDok

Eingang zum Volltext in SciDok

Lizenz

Dissertation zugänglich unter
URN: urn:nbn:de:bsz:291-scidok-69639
URL: http://scidok.sulb.uni-saarland.de/volltexte/2017/6963/


Logics for rule-based configuration systems

Tang, Ching Hoo

pdf-Format:
Dokument 1.pdf (1.375 KB)

Bookmark bei Connotea Bookmark bei del.icio.us
SWD-Schlagwörter: Logik , Verifikation , Regel , Formalisierung
Freie Schlagwörter (Deutsch): Regelbasierte Konfigurationssysteme , DOPLER , PIDL
Freie Schlagwörter (Englisch): logic , verification , rules , formalization , configuration
Institut: Max-Planck-Institut für Informatik
Fakultät: Fakultät 7 - Naturwissenschaftlich-Technische Fakultät II
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Hauptberichter: Weidenbach, Christoph (Prof. Dr.)
Sprache: Englisch
Tag der mündlichen Prüfung: 16.08.2017
Erstellungsjahr: 2017
Publikationsdatum: 12.10.2017
Kurzfassung auf Englisch: Rule-based configuration systems are being successfully used in industry, such as DOPLER at Siemens. Those systems make complex domain knowledge available to users and let them derive valid, customized products out of large sets of components. However, maintenance of such systems remains a challenge. Formal models are a prerequisite for the use of automated methods of analysis. This thesis deals with the formalization of rule-based configuration. We develop two logics whose transition semantics are suited for expressing the way systems like DOPLER operate. This is due to the existence of two types of transitions, namely user and rule transitions, and a fixpoint mechanism that determines their dynamic relationship. The first logic, PIDL, models propositional systems, while the second logic, PIDL+, additionally considers arithmetic constraints. They allow the formulation and automated verification of relevant properties of rule- based configuration systems.
Kurzfassung auf Deutsch: Regelbasierte Konfigurationssysteme werden erfolgreich in der Industrie benutzt, wie etwa DOPLER bei Siemens. Diese Systeme machen komplexes Domänewissen Anwendern verfügbar und erlaubt es ihnen, gültige, angepasste Produkte aus großen Mengen von Teilen zu erstellen. Allerdings bleibt die Wartung solcher Systeme eine Herausforderung. Formale Modelle sind Voraussetzung für den Einsatz automatisierter Analysemethoden. Diese Arbeit beschäftigt sich mit der Formalisierung von regelbasierter Konfiguration. Wir entwickeln zwei Logiken, dessen Transitionssemantiken dafür geeignet sind, die Art und Weise, auf der Systeme wie DOPLER operieren, abzubilden. Dies ist möglich durch die Existenz von zwei Typen von Transitionen, nämlich User- und Regeltransitionen, und eines Fixpunktmechanismus, der ihre dynamische Beziehung bestimmt. Die erste Logik, PIDL, modelliert propositionale Systeme, während die zweite Logik, PIDL+, zusätzlich arithmetische Constraints betrachtet. Sie erlauben die Formulierung und automatische Verifikation relevanter Eigenschaften regelbasierter Konfigurationssysteme.
Lizenz: Veröffentlichungsvertrag für Dissertationen und Habilitationen

Home | Impressum | Über SciDok | Policy | Kontakt | Datenschutzerklärung | English