Constraint Handling Rules (CHR)

Constraint Handling Rules (CHR) is a concurrent committed-choice constraint logic programming language consisting of guarded rules that transform multi-sets of atomic formulas (constraints) until exhaustion. It was designed by Thom Frühwirth in 1991.

CHR can embed many rule-based formalisms and systems, and it can describe algorithms in a compact declarative way without compromising efficiency. The clean semantics of CHR ensures that several desirable properties hold for CHR programs and also facilitates sophisticated program analysis. Dozens of CHR libraries exist for programming languages such as Prolog, Java and Haskell.

So far, worldwide more than 200 academic and industrial projects use CHR and 2000 research publications investigate CHR. There is a yearly workshop and a biannual summer school on CHR.

Constraint-Programmierung und Schliessen mit Constraints

Die Constraint-basierte Programmierung begann vor etwa 10 Jahren als natürliche Fusion zweier deklarativen Paradigmen: Lösen von Constraints und Logikprogrammierung. Dadurch lassen sich schnell und elegant komplexe kombinatorische Probleme durch eine Verbindung aus Constraintlösen und Suche behandeln.

Unter Constraintlösen versteht man das Lösen von Problemen, indem man Constraints (Bedingungen, Einschränkungen) angibt, die von einer Lösung erfüllt werden müssen, und diese Constraints kombiniert, um die Lösung weiter einzuschränken.

Haupteinsatzbereiche sind Produktions- und Personalplanung, Transportoptimierung sowie Layoutgenerierung. Dieses Projekt untersucht verschiedenste Apekte der Constraint-Programmierung.

Weitere Informationen

Buch Constraint-Programmierung

ConMEq

Automatic Support for Proving Confluence Modulo Equivalence for CHR

Experimentelles Software-Engineering

Grundlage für eine systematische und nachvollziehbare Qualitätsverbesserung in der Softwareentwicklung bildet eine in messbarer Form vorliegende Beschreibung der zu erreichenden Qualitätsziele. Nur auf einer derartigen, quantitativen Basis ist es möglich, die Ausprägung von Qualitätsmerkmalen in Prozess und Produkt objektiv zu bestimmen und zur Planung, Steuerung und Kontrolle der Softwareentwicklung zu verwenden. Vor diesem Hintergrund werden (meist in Kooperation mit dem Daimler-Chrysler-Forschungszentrum Ulm) aktuelle Themen im Bereich Software für technische Systeme, insbesondere ihre systematische Entwicklung und analytische Qualitätssicherung, experimentell untersucht mit dem Ziel, verlässliches Zahlenmaterial zu gewinnen.

Integration konventioneller und formaler Methoden der Softwaretechnik

Die Notwendigkeit des Einsatzes formal fundierter Methoden in der Softwareentwicklung, z.B. bei sicherheitskritischer Software, als Alternative zum (konventionellen) Software-Engineering wird zunehmend erkannt und akzeptiert, da dadurch z.B. eine frühzeitige Simulation, Verifikation und eine automatische Testfallgenerierung möglich wird. Andererseits haben sich auch Erkenntnisse und Vorgehensweisen des (konventionellen) Software-Engineering in der Praxis bewährt. Ziel ist es daher, durch Symbiose und Integration von konventionellen "best practices" und formalen Methoden des Software-Engineering die jeweiligen Vorteile beider Ansätze zu kombinieren um so zu einer durchgängigen Methodik der Softwareentwicklung im Sinne einer allgemein akzeptierten Konstruktionslehre zu kommen. Neben theoretischen und methodischen Aspekten umfaßt dies auch Werkzeuge und Anwendungen.

Ensure

ENsurance of Software evolUtion by Run-time cErtification

Model Driven Development

Viele der heutigen Softwaremodellierungstools sind für Entwickler nicht oder nur wenig hilfreich, da sie oft als reine Dokumentationswerkzeuge benutzt werden oder nur Codegerüste aus statischen Modellen erzeugen können. Die Folge ist, dass Modelle aus den Analyse- und Entwurfsphasen während der Implementierung nicht mehr ausreichend gepflegt werden und somit die Modelle nicht mehr das aktuelle Design des Codes reflektieren. Wir beschäftigen uns mit der Frage, wie mächtigere Software-Werkzeuge konstruiert werden können, welche die Synchronisation von Analyse/Entwurfs- und Implementierungsartefakten unterstützen bzw. sicherstellen können ohne den Entwickler in seinen bisherigen Implementierungsmöglichkeiten zu sehr einzuschränken.
Einige der Themen in diesem Umfeld sind:

  • MDD (Model Driven Development): Codegenerierung und Metamodellierung
  • MDA (Model Driven Architecture)
  • Verhaltensmodellierung und -simulation mit der UML 2.0
  • Compilerbau
  • Enterprise Design Patterns

ActiveCharts

Interpreter und Debugger für UML 2 Aktivitätsdiagramme

Programmtransformation / Ultra

Programmtransformation charakterisiert eine Methodik der Softwareentwicklung bei der man aus einer formalen, meist funktional-deklarativen Spezifikation durch schrittweise Anwendung semantiktreuer Umformungsregeln ein Programm ableitet, das nicht nur per Konstruktion korrekt ist, d.h. die Spezifikation erfüllt, sondern auch weiteren wichtigen Kriterien wie etwa Effizienz genügen kann.
Konkretes Ergebnis der Anwendung dieses Ansatzes auf die funktionale Programmierung ist das interaktive, prototypische Transformationssystem Ultra, das eine gute Basis für weitere Studien im Rahmen der formalen Programmentwicklung bietet.

Fλux

Visualisierung von Haskell Programmen als Datenfluss Diagramme

Requirements Engineering

Requirements-Engineering beschäftigt sich mit Methoden, Formalismen und Werkzeugen zur Ermittlung, Formulierung und Prüfung von Anforderungen an Software-gestützte Systeme. Zentral bei unseren Aktivitäten im Requirements-Engineering steht die Idee der Modellbildung, d.h. die abstrakte, weitgehend formale Beschreibung eines Systems in einer Form, die es ermöglicht, einerseits Anforderungen entsprechend zu präzisieren (ohne die Implementierung vorwegzunehmen) und andererseits Systemstrukur und -verhalten zum frühest möglichen Zeitpunkt im Rahmen einer Systementwicklung studieren, analysieren und benutzen zu können.
Konkret betrachtete Fragestellungen sind:

  • Grundlagen, Zusammenhänge, Schnittstellen und Integration verschiedener bestehender Ansätze
  • Koexistenz und Mischung verschiedener Formalismen
  • Konsistenz- und Vollständigkeitskriterien für Modelle oder präzise semantische Definitionen einzelner Modellierungskonzepte
  • Methodik und Rechnerunterstützung bei der Entwicklung von (formalen) Spezifikationen aus informellen Problemstellungen
  • Einsatz formal fundierter Methoden
  • allgemeine Aspekte der Werkzeugunterstützung für das Requirements-Engineering