Gerichtete und parallele Validierung von abstrakten Spezifikationen

点击翻译按钮获取中文摘要

Formale Methoden haben das Ziel fehlerfreie Software zu produzieren. Die B-Methode ist eine formale Methode die erfolgreich in mehreren Industrie-Projekten angewandt wurde. Mit steigender Komplexität industrieller Anforderungen an Softwaresysteme wird auch das Erstellen korrekter Spezifikationen schwieriger. Jeder Fehler in der Ausgangsspezifikation tritt auch in der resultierenden Software auf, daher stellt die Korrektheit der Spezifikation einen kritischen Punkt dar. Das Hauptziel dieses Forschungsprojektes ist es, Methoden und Werkzeuge zu entwickeln, mit denen aus Industrieprojekten stammende, komplexe, formale B-Spezifikationen validiert werden können. Eine besondere Herausforderung dabei ist die hohe Ausdruckskraft der B Spezifikationssprache. Wir glauben, dass gerade in dieser hohen Abstraktionsebene ein großes Potential für intelligente Validierungstechniken steckt. In diesem Projekt wollen wir folgende zwei Techniken entwickeln: gerichtetes Modelchecking von B, um Fehlerzustände in großen Zustandsräumen anhand von Heuristiken zu finden, sowie paralleles Modelchecking, zur Verteilung des Rechenaufwandes. Beide Techniken sollen durch genetische Optimierung und statische Analyse unterstützt werden.