Bachelor-/Masterthesis Themen: Verifikation verteilter Systeme mit dem interaktiven Theorembeweiser Isabelle

Das Ziel dieser Arbeiten ist Datenstrukturen, Funktionen und Prinzipien zu entwickeln, um verteilte, asynchron kommunizierende Systeme zu verifizieren. Verteilte Systeme begegnet man zB. bei Bussystemen im Auto, Telekommunikationsnetzen oder beim Internet. Solche Systeme neigen dazu, komplexer und fehleranfälliger zu sein als sequentieller Software. Systemüberprüfung wird verwendet um festzustellen, ob ein Entwurf oder ein Produkt bestimmte Eigenschaften besitzt. Das System wird als “korrekt” bezeichnet, wenn alle von seiner Spezifikation erhaltenen Eigenschaften erfüllt werden.

Formale Methoden helfen dabei, Unklarheiten bei Spezifikationen zu beseitigen, um dann Verifikation zu betreiben. Für die systematische, formale Spezifikation und Entwicklung von verteilten interaktiven Systemen und deren Komponenten wurde in den 90‘ Jahren die Spezifikationstechnik FOCUS entwickelt.

In diesen Arbeiten werden verteilte Systeme mit der Spezifikationstechnik FOCUS beschrieben und mit Hilfe des interaktiven Theorembeweisers Isabelle verifiziert, der eine ähnliche Syntax wie Funktionale Programiersprachen verwendet. Theorembeweiser erfordern Hinweise für die Beweissuche, die von einem menschlichen Benutzer dem Beweissystem gegeben werden müssen. Abhängig vom Automatisierungsgrad kann ein Theorembeweiser im Wesentlichen selbstständig bedeutsame Teile der Beweissuche automatisch durchführen.

Wir bieten die Möglichkeit einen aktiven Beitrag zur Forschung zu leisten und einen Einblick in internationale Forschungsprojekte zu bekommen. Demo: https://www.youtube.com/watch?v=krl4Q7MAAlo

Notwendige Vorkenntnisse:

• Spaß an Mathematik

Ansprechpartner

Interesse an dem Thema? Informieren Sie sich mit unseren Publikationen über unsere aktuelle Forschung.

Für mehr Informationen wenden Sie sich mit ihren Bewerbungsunterlagen bitte an Dipl.-Inform. Deni Raco.

Aufgabenstellung:

Prof. Dr. Bernhard Rumpe
Lehrstuhl Software Engineering
Ahornstr. 55
52074 Aachen