Refine
Document Type
- Doctoral thesis (4)
Has Fulltext
- yes (4)
Is part of the Bibliography
- no (4)
Keywords
- Verifikation (4) (remove)
Rules are a critical technology component for the early adoption and applications of knowledge-based techniques in e-business, especially enterprize integration and B2B ecommerce. They also play an important role in information systems engineering, especially in the specification of functional requirements where business rules are the foundation for capturing and modeling business application logic. When using rules, companies may encounter obstacles with two issues: The problem of rule interoperability, which is caused by a variety of rule languages and rule systems, and the problem of rule quality as a consequence of a large amount of business rules created and used in an organization. A particular solution to the rule interoperability problem is a standardized way of performing rule interchange between different rule languages and tools. The thesis addresses the problem by considering a rule interchange mapping from the Object Constraint Language (OCL) into the Semantic Web Rule Language (SWRL). This mapping is useful for various communities. For instance, software developers, who actively use UML/OCL, may employ the mapping in order to translate their rules to SWRL and use them in a Semantic Web application. On the other hand, the research on rule interchange is interesting for Semantic Web practitioners, who work in the area of formal semantics of rule languages and have interest in the rule interchange standardization. The main contribution of the thesis concerning rule interchange is the proof of correctness of the mapping from the semantical point of view. The problem of semantic correctness of rule interchange mapping is formulated for two rule languages and solved for OCL and SWRL. The approach can be applied to other rule languages with formal semantics. The quality of rules is high if they are expressed in the right way and express what business people want to express. However, due to various reasons, for instance communication problems between business people and rule modelers, rules may become inconsistent, incomplete or redundant. Therefore, organizations need rule quality measurement and technologies to improve the quality. A particular way to control and to improve the rule quality is by means of rule verification. In this respect, the main contribution of the thesis is the declarative rule verification approach, which can be used for detection of different problems in rule bases. The verification approach is implemented for Jena rules, which makes it more applicable for the quality control of upcoming Semantic Web rule-based applications.
Diese Arbeit widmet sich der Verifikation nebenläufiger Systeme unter Verwendung von Modelcheckingverfahren. Es wurden Modelcheckingverfahren betrachtet und entwickelt, welche die drei Gebiete: Petrinetze als Modellierungssprache, linear-time temporale Logik zur Spezifikation von Systemeigenschaften und binäre Entscheidungsgraphen zur Repräsentation großer Zustandsmengen verbinden. Bei der Entwicklung von Modelcheckingverfahren wurde darauf geachtet, dass durch die Kombination der einzelnen Gebiete deren Vorteile erhalten bleiben und die sich zwischen den Gebieten ergebendnen Synergien ausgenutzt werden. Den wesentlichen innovativen Teil der Arbeit stellt die Entwicklung eines LTL-Modelcheckingverfahrens dar, welches eine symbolische Repräsentierung der Zustände mit einem on-the-fly Verifikationsverfahren verbindet und dabei eine zeitliche Komplexität der klassischen LTL-Modelcheckingverfahren erreicht.
Diese Arbeit behandelt einen Ansatz zur Verifikation verteilter Systeme. Zur Beschreibung des Verhaltens solcher Systeme verwenden wir die sog. Semiwörter, die eine spezielle Form von pomsets darstellen, sowie Mazurkiewiczspuren. Wir weisen nach, daß jedes nebenläufige System (d. h. ein System, für dessen Aktionen eine Unabhängigkeitsrelation angegeben werden kann) als verteiltes System aufgefaßt werden kann. Wir beschreiben eine endliche Repräsentation des Verhaltens nebenläufiger und verteilter Systeme, die auf dem Begriff des Prozeßautomaten beruht, und geben Algorithmen zur Konstruktion derartiger Prozeßautomaten an. Schließlich definieren wir die verteilte, agentenbasierte temporale Logik DCTL. Die Beschreibung eines Modelcheckers für diese Logik, der auf Prozeßautomaten operiert, schließt die Arbeit ab.
Die Konstruktion eingebetteter Systeme, die starke Realzeit-Anforderungen zu erfüllen haben, wird in den verschiedensten Anwendungsbereichen immer bedeutsamer, z. B. in der Medizin, der Transporttechnik oder der Produktionsautomatisierung. Formale Methoden unterstützen die fehlerarme Entwicklung solcher Systeme, weil sie auf einer präzisen mathematischen Grundlage aufbauen. Der Autor entwickelt einen geeigneten Modellierungsformalismus und effiziente Verifikationsverfahren für den Einsatz einer formalen Methode. Durch die Einführung eines Modulkonzepts wird die Modellierung auch großer Realzeit-Systeme systematisch unterstützt. Für die Verifikation werden effiziente BDD-basierte Algorithmen verwendet, wobei auch das Problem des Findens guter BDD-Variablenordnungen gelöst wird. Es werden sowohl Erreichbarkeitsanalyse als auch Verfeinerungsanalyse unterstützt. Die Praktikabilität der Ansätze zur Modellierung und Verifikation werden in verschiedenen Fallstudien aus den Bereichen der reaktiven Systeme und der Kommunikationsprotokolle demonstriert.