Logo des Repositoriums

Auflistung nach Autor:in "Steffen, Bernhard"

1 - 1 von 1
  • Konferenzbeitrag
    Datenflussanalyse als Modelchecking im jABC
    (Software Engineering 2006, Proceedings der Fachtagung des GI-Fachbereichs Softwaretechnik, 2006) Lamprecht, Anna-Lena; Margaria, Tiziana; Steffen, Bernhard
    Dieses Papier beschreibt wie das jABC (eine generische Umgebung für bibliotheksbasierte Programmentwicklung) zusammen mit zwei seiner Plugins (der Modelchecker und ein Flussgraph-Konverter) ein Framework, DFA-MC, für intraprozedurale Datenflussanalyse als Modelchecking bildet. Basierend auf Funktionalitäten, die von der Programmanalyseplattform Soot bereitgestellt werden, generiert der Konverter Graphstrukturen aus Java-Klassen. Die Datenflussanalysen werden dann als Formeln im modalen μ-Kalkül ausgedrückt. Die Analyse selbst wird ausgeführt, indem der Modelchecker die Gültigkeit der Formel auf dem Flussgraphen überprüft.