Logo des Repositoriums
 
Konferenzbeitrag

Datenflussanalyse als Modelchecking im jABC

Lade...
Vorschaubild

Volltext URI

Dokumententyp

Text/Conference Paper

Zusatzinformation

Datum

2006

Zeitschriftentitel

ISSN der Zeitschrift

Bandtitel

Verlag

Gesellschaft für Informatik e.V.

Zusammenfassung

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.

Beschreibung

Lamprecht, Anna-Lena; Margaria, Tiziana; Steffen, Bernhard (2006): Datenflussanalyse als Modelchecking im jABC. Software Engineering 2006, Proceedings der Fachtagung des GI-Fachbereichs Softwaretechnik. Bonn: Gesellschaft für Informatik e.V.. PISSN: 1617-5468. ISBN: 3-88579-173-0. pp. 125-130. Regular Research Papers. Leipzig. 28.-31. März 2006

Schlagwörter

Zitierform

DOI

Tags