Direkt zum Inhalt | Direkt zur Navigation

Eingang zum Volltext

Lizenz

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:bsz:25-opus-87991
URL: http://www.freidok.uni-freiburg.de/volltexte/8799/


Berstel-Da Silva, Bruno

Verification of business rules programs

Verifikation von Geschäftsregel-Programmen

Dokument1.pdf (1.488 KB) (md5sum: ff213ab3e19e73c598cd401cd31cf246)

Kurzfassung in Englisch

The technical contribution of the thesis is to present—to the best of our knowledge, for the first time—an approach to the formal verification of business rules programs. We propose a verification method for proving correctness properties for a business rules program in a compositional way. The approach enables rule authors and tool developers to understand, express formally, and prove, properties of the execution behavior of business rules programs. The conceptual contribution of this thesis is to present the enabling framework for treating business rules as a topic of scientific investigation in semantics and program verification.

Multitier architectures increasingly use business rules to encode the application tier (the so-called business logic). The authoring and the execution of business rules programs is supported by a Business Rules Management System (BRMS). A business rules program consists in a set of mutually independent rules, that is, conditional update statements authored in a modular, case-by-case approach. A business rules program is declarative in that it does not specify the control flow; the set of rules are executed on a set of objects, exhaustively for each rule and each object, in any order.

Until now, the emphasis in research has been on optimizing the efficient execution of business rules programs by a BRMS. A variety of compilation and execution schemes have been developed, including the well-known Rete algorithm. The verification of business rules programs has been neglected as a topic of scientific research. The need for correctness is, however, no less obvious for business rules programs than it is for safety-critical systems, even though the risks at stake are economic and usually not life-threatening.

The thesis is structured in three main parts. In the first part, we present a formal definition of the execution behavior of business rules programs. In the second part of the thesis, we introduce correctness specifications for business rules programs. In the third and final part, we propose a compositional verification method for business rules programs.

In a non-technical appendix to the thesis, we demonstrate the practical potential of our formal approach in the context of an existing commercial Business Rules Management System. This BRMS comes with a lightweight analysis engine (named “Rule Static Analysis”). We show that its various analysis and verification features can be given a solid foundation thanks to the approach to the formal verification of business rules programs presented in this thesis.


Kurzfassung in Deutsch

Der Beitrag dieser Arbeit ist der (unserem Wissen nach) erste formale Ansatz zur Verifikation von Geschäftsregel-Programmen. Wir schlagen eine Verifikationsmethode vor, um die Korrektheit von Geschäftsregel-Programmen kompositionell zu beweisen. Der Ansatz ermöglicht Autoren von Geschäftsregeln und Entwicklern einer Werkzeugumgebung, Eigenschaften der Ausführung von Geschäftsregel-Programmen zu verstehen, formal zu beschreiben und zu beweisen.

Der übergeordnete Beitrag der Arbeit ist, die logischen Grundlagen bereit zu stellen, um Geschäftsregeln überhaupt erst als Gegenstand der wissenschaftlichen Untersuchung in Semantik und Verifikation einführen zu können. Schichtenarchitekturen benutzten in wachsendem Maße die sogenannten Geschäftsregeln, um die Logikschicht (auch: Businessschicht) zu kodieren. Die Erfassung und die Ausführung von Geschäftsregel-Programmen wird durch ein Geschäftsregel-Managementsystem (GRMS) unterstützt. Ein Geschäftsregel-Programm besteht aus einer Menge von voneinander unabhängigen Regeln, d.h., bedingten Zuweisungsinstruktionen, die in einem modularen, Fall-basierten Ansatz gesammelt werden. Ein Geschäftsregel-Programm ist deklarativ in dem Sinne, dass es nicht den Kontrollfluss spezifiziert; die Regeln werden auf der gegebenen Menge von Objekten ausgeführt, nach und nach für jede Regel und jedes Objekt, in nicht-festgelegter Reihenfolge.

Die wissenschaftliche Forschung hat sich bisher auf die Effizienz der Ausführung von Geschäftsregel-Programmen durch ein GRMS konzentriert. Eine Vielfalt von Kompilierungs- und Ausführungsschemas sind entwickelt worden, so insbesondere der bekannte Rete-Algorithmus. Die Verifikation von Geschäftsregel-Programmen wurde bisher als Gegenstand wissenschaftlicher Forschung vernachlässigt. Der Bedarf an Korrektheit ist jedoch für Geschäftsregel-Programme nicht weniger einleuchtend als für sicherheitskritische Systeme, auch wenn die auf die Spiel stehenden Risiken ökonomisch sind, und üblicherweise nicht lebensbedrohlich.

Die Arbeit besteht aus drei Hauptteilen. Im ersten Teil präsentieren wir eine Formalisierung des Ausführungsverhaltens von Geschäftsregel-Programmen. Im zweiten Teil der Arbeit führen wir Korrektheitsspezifikationen für Geschäftsregel-Programmen ein. Im dritten und letzten Teil der Arbeit führen wir eine kompositionelle Verifikationsmethode
für Geschäftsregel-Programme ein.

In einem nicht-technischen Anhang zu dieser Arbeit demonstrieren wir das praktische Potential unseres Ansatzes im Kontext eines existierenden kommerziellen Geschäftsregel-Managementsystems. Dieses GRMS verfügt über ein leichtgewichtiges Analyse-Modul (unter dem Namen “Rule Static Analysis”). Wir zeigen, dass den verschiedenen Analyse- und Verifikationsfunktionalitäten des GRMS dank des in dieser Arbeit vorgestellten Ansatzes zur formalen Verifikation eine solide Fundierung gegeben werden kann.


SWD-Schlagwörter: Verifikation , Geschäftsregel , Axiomatische Semantik , Hoare-Logik
Freie Schlagwörter (deutsch): Geschäftsregel-Managementsystem , GRMS
Freie Schlagwörter (englisch): Program verification , Business Rules , Hoare logic , Rule programming , BRMS
CCS Klassifikation F.3.1 Spec
Institut: Institut für Informatik
Fakultät: Technische Fakultät (bisher: Fak. f. Angew. Wiss.)
DDC-Sachgruppe: Technik
Dokumentart: Dissertation
Erstgutachter: Podelski, Andreas (Prof. Dr.)
Sprache: Englisch
Tag der mündlichen Prüfung: 11.07.2012
Erstellungsjahr: 2012
Publikationsdatum: 27.11.2012
Indexliste