Komponentenarchitekt... Forschungsprojekte Einsatz statistische...

Masterarbeit

Untersuchung verschiedener Model Checking Werkzeuge bzgl. ihrer Eignung für den Einsatz in der Telekommunikation

 

Zusammenfassung

Model Checking bezeichnet den automatischen Nachweis bzw. die automatische Widerlegung der Gültigkeit formal beschriebener Systemeigenschaften. Dadurch lassen sich bereits in frühen Phasen der Softwareentwicklung Spezifikationsfehler aufdecken.

Ziel dieser Diplomarbeit ist es, zunächst ein Kriterienkatalog zu definieren, anhand dessen die Eignung verschiedener Model Checkers zur Validierung von Telekommunikationssystemen zu bewerten ist. Insbesondere ist auf die Unterschiede der Werkzeuge bezüglich der Ausdrucksstärke der zugrundeliegenden Formalismen (System- und Eigenschaftsmodellierung, etwa unter Berücksichtigung der Erfaßbarkeit der Zeit, des Zufalls, maximaler Pfadlängen, etc.), sowie weiterer Werkzeugeigenschaften, wie etwa Performance, GUI, etc.) vergleichend einzugehen.

Zur Visualisierung ist ein Werkzeug zu implementieren, das graphische Darstellungen von Systemmodellen anhand von Blockdiagrammen, sowie deren Bearbeitung derart ermöglicht, daß Letztere als Eingabe für das am Lehrstuhl verfügbare Model Checker NuSMV, sowie für einen zusätzlichen Model Checker höherer Ausdruckstärke dienen kann. Bei Verwendung von Modellen, die auf einer tabellarischen Systemdarstellung basieren, hat dieses Werkzeug darüber hinaus auch die Konsistenz zwischen beiden Darstellungsarten (Diagrammen und Tabellen) zu sichern.

Betreuer: Dipl.-Inf Marc Spisländer

In Kooperation mit: Lucent Technologies