ISSE

Search

Formal Analysis and Software Architectures for Trustworthy Organic Computing @ OC-Trust


Start date: 01.10.2009
Funded by: DFG (Deutsche Forschungsgemeinschaft)
Local project leader: Prof. Dr. Wolfgang Reif
Local scientists: Dr. Hella Ponsar (geb. Seebach)
External scientists / cooperations: Prof. Dr. Theo Ungerer
Prof. Dr. Christian Müller-Schloer
Prof. Dr. Jörg Hähner
Prof. Dr. Elisabeth André
Publications: Publication list

Abstract

OCTRUSTLogo In ForSa@OC-Trust werden formale Methoden, Software-Engineering-Ansätze und Algorithmen für vertrauenskritische Organic Computing Systeme entwickelt. Dabei steht die Gewährleistung funktionaler Korrektheit und Safety im Vordergrund. Die Arbeiten beinhalten formale Modellierung und Analyse von vertrauenskritischen Systemen und Methoden zur Beobachtung von Systemen zur Laufzeit. Weiterhin wird untersucht, wie sich die Konstruktion vertrauenskritischer Organic Computing Systeme standardisieren und vereinfachen lässt und wie sich Maßnahmen zur Gewährleistung von Vertrauenswürdigkeit in den Entwicklungsprozess integrieren lassen. Schließlich werden Algorithmen, die Vertrauenswerte einbeziehen und deren Korrektheit gezeigt werden kann, entwickelt und in vertrauenskritischen Szenarien eingesetzt. Eine Anwendungsplattform aus dem Energiebereich, das Trusted Energy Grid, und die darauf aufbauende Anwendung "Autonome Virtuelle Kraftwerke" dienen der Evaluation und Demonstration der entwickelten Techniken.

Description

Informationen für Studenten: Abschlussarbeiten; Praxis-, Forschungs- und Projektmodule, Hiwitätigkeiten

Systeme, die sich selbst organisieren, die dynamisch zur Laufzeit ihre Struktur verändern und die in Umgebungen eingesetzt werden, deren dynamische Entwicklung unvorhersehbar ist, können nicht mit klassischen Software-Engineering-Methoden konstruiert und analysiert werden. Insbesondere, wenn ein System missions-kritisch ist, also unter keinen Umständen ausfallen oder Schaden verursachen darf, muss sichergestellt sein, dass Funktionalität und Betriebssicherheit und damit ihre Vertrauenswürdigkeit gewähreleistet sind. Besondere Herausforderungen stellen dabei die Unsicherheit über die Umgebung und die komplexe, sich verändernde Struktur der Systeme dar. Ein Beispiel für eine Domäne, in der solche Systeme eingesetzt werden könnten, ist das Energiemanagement und insbesondere die dezentrale Steuerung der Energieversorgung.

Um die Herausforderungen handhabbar zu machen, werden in ForSA@OC-Trust Methoden entwickelt, die es ermöglichen, formale Aspekte, Softwaretechnik und Algorithmik für vertrauenskritische Organic Computing Systeme miteinander zu verbinden. Dabei werden drei konkrete Ziele verfolgt:

1. Kontrolle emergenten Verhaltens durch Korrektheits- und Safety-Betrachtungen zur Laufzeit und Designzeit

Die Systemfunktionalität vertrauenskritischer OC-Systeme ergibt sich  aus den Interaktionen einer großen Anzahl von Elementen. Vertrauensaspekte spielen eine wichtige Rolle im Zusammenspiel der Elemente, insbesondere bei Interaktionen zwischen unbekannten Partnern. Hinzu kommen noch die große Heterogenität der Systeme und ihre Offenheit. Daher ist es sehr schwierig, Korrektheits- und Safety-Betrachtungen für das Gesamtsystem zur Designzeit durchzuführen.

Alternativ lässt sich allerdings mit Hilfe von Laufzeitverifikation die Korrektheit des Systems sicherstellen. Als Grundlage dient dabei die Spezifikation eines weichen Verhaltenskorridors, der die Bedingungen definiert, unter denen das System korrekt funktioniert und es erlaubt, Beziehungen zwischen diesen Bedingungen anzugeben. Außerdem lassen sich gezielte Gegenmaßnahmen mit der Verletzung der Bedingungen verbinden.

Ähnlich wie bei funktionaler Korrektheit ist es aber auch bei Safety schwierig, in einer offenen, heterogenen, dynamischen Umgebung im Voraus Analysen durchzuführen. Daher wird an dynamischen Safety-Modelle geforscht, die zur Laufzeit erstellt und analysiert werden können.

Durch die Interaktion zwischen Agenten in Organic Computing Systemen entstehen implizit oder explizit Subsysteme bzw. Hierarchien innerhalb derer die Agenten gekapselt sind (Systems of Systems). In vielen Fällen ist es nicht so, dass das Ziel der einzelnen Agenten auch dem Ziel des Subsystems entspricht,  zu dem sie gehören, oder gar dem Ziel des Gesamtsystems. In ForSA@Oc-Trust wird deshalb an den Zusammenhängen zwischen Zielen auf verschiedenen Systemebenen und den für die einzelnen Ebenen definierten Bedingungen geforscht.

2. Prozesse und Methoden für vertrauenskritische Organic Computing Systeme

Zur Sicherstellung der Vertrauenswürdigkeit in vertrauenskritischen Organic Computing Systemen ist es erforderlich, vertrauensbildende Maßnahmen schon beim Entwurf dieser Systeme einzuleiten und sinnvoll einzusetzen. Da bisherige Software-Entwicklungsmethoden entweder nicht anwendbar sind oder die Anforderungen nur unzureichend erfüllen, werden Methoden und ein Prozess entwickelt, die gemeinsam die systematische Konstruktion vertrauenskritischer Organic Computing Systeme ermöglichen.

In diesem Zusammenhang werden Referenzarchitekturen für die in den Fallstudien entwickelten Einsatzgebiete definiert sowie Patterns für den Umgang mit Vertrauenswerten und für Mechanismen zur Steigerung der Ausfallsicherheit und Datensicherheit erstellt. Auf dieser Grundlage wird eine Guideline spezifiziert, die vorgibt, wie diese in existierenden Software-Entwicklungsmethoden eingesetzt werden müssen, um wirksam Vertrauenswürdigkeit zu erzielen. Unter Einbeziehung formaler Aspekte und der hierarchischen Organisation der betrachteten Systeme wird daraus dann ein Leitfaden für die Konstruktion vertrauenskritischer Organic Computing Systeme entstehen.

3. Umgang mit Unsicherheit in Algorithmen

Optimierungsverfahren müssen in vielen Fällen auf Vorhersagen über die zukünftige Entwicklung eines Systems zurückgreifen. Jedoch sind diese Vorhersagen in der Regel fehlerhaft und führen deshalb zu schlechten oder unbrauchbaren Ergebnissen, was besonders in sicherheitskritischen Systemen ein großes Problem darstellen kann. Außerdem kann der Fehler von Vorhersage zu Vorhersage variieren. Bei Ausfall von Systemkomponenten, die bei der Optimierung mit einbezogen wurden, müssen deren Aufgaben von anderen Systemkomponenten übernommen werden, um das System weiterhin stabil zu betreiben. Genauso können aber auch während der Laufzeit neue Komponenten hinzukommen, wodurch das System eine andere Struktur aufweist als zum Zeitpunkt der Durchführung der Optimierung angenommen.

Um mit diesen Problemen umgehen zu können, werden in ForSA@OC-Trust Methoden entwickelt, die mit Hilfe von Vertrauenswerten die Unsicherheit quantifizierbar machen und diese Werte in Optimierungs- oder Strukturierungsalgorithmen einbeziehen.

Fallstudie: Dezentrale Steuerung der Energieversorgung

Alleine in Bayerisch Schwaben sind im Februar 2011 fast 58000 Stromerzeugungsanlagen in Betrieb,  die von regenerativen Energien abhängen und nicht oder nur eingeschränkt steuerbar sind (Quelle). Die mit dieser riesigen Anzahl von Kraftwerken und der Unvorhersagbarkeit der Energiequellen eingeführten Probleme bei der Regelung der Stromerzeugung sind zentrale Herausforderungen bei der von der Bundesregierung angestrebten Umstellung des Energiemixes hin zu regenerativen Energien.

Im Rahmen dieses Arbeitspaketes wurde die Anwendung "Autonome Virtuelle Kraftwerke" entwickelt,  mit deren Hilfe die dezentrale Steuerung einer großen Anzahl von Stromerzeugern durchgeführt werden kann. Die Fallstudie stellt als betriebssicherheits- und missions-kritisches System besondere Ansprüche an die Vertrauenswürdigkeit. Anhand der Fallstudie werden die Ergebnisse von ForSA@OC-Trust evaluiert.

Weitere Informationen zur Fallstudie finden Sie hier.

Links: