WERKZEUGE

Werkzeuge für quantitative Systemevaluierung

Die Forschung der Gruppe hat auch eine praktische Dimension: Ohne Tool-Unterstützung bleibt sie im Elfenbeinturm. Wir beschäftigen uns mit der Entwicklung verbesserter Model Checker für stochastische Systeme.

 

Ein Großteil der Anstrengungen in der Tool-Entwicklung in die Verbesserung der Unterstützung der Sprache MODEST investiert. Das bis jetzt wichtigste Resultat ist das MODEST IDE für probabilistische Systeme mit Zeitinformationen.

 

PASS ist ein Model Checker für probabilistische Systeme. Er basiert auf Prädikatenabstraktion und automatischer Verbesserung der Abstraktion. Diese baut auf der Analyse (falscher) Gegenbeispiele in der Abstraktion auf.

 

PASS hat zwei Schwestern: INFAMY und PARAM. Alle drei akzeptieren praktisch die selbe Sprache, haben aber unterschiedliche Stärken. Die Modelle, die PARAM behandeln kann sind Markov-Ketten mit Parametern, während INFAMY der erste Model Checker für Markov-Ketten mit unendlich vielen Zuständen in kontinuierlicher Zeit ist.

 

FlowSim ist ein Benchmark-Programm für verschiedene Implementierungen und Optimierungen von Algorithmen um die größte Relation zwischen den Zuständen eines probabilistischen Modells zu berechnen. Das Tool kann auch als Generator für zufällige Modelle verwendet werden. Der Quellcode für FlowSim steht zur Verfügung.

 

ProHVer ist ein Werkzeug um Eigenschaften von probabilistischen hybriden Systemen zu berechnen.

 

APHzip ist eine Sammlung von Werkzeugen, um azyklische Phase-Typ-Darstellungen zu erzeugen, manipulieren, und minimieren.