Datenflussanalyse als Modelchecking im jABC

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.
  • Vollständige Referenz
  • BibTeX
Lamprecht, A.-L., Margaria, T. & Steffen, B., (2006). Datenflussanalyse als Modelchecking im jABC. In: Biel, B., Book, M. & Gruhn, V. (Hrsg.), Software Engineering 2006, Proceedings der Fachtagung des GI-Fachbereichs Softwaretechnik. Bonn: Gesellschaft für Informatik e.V.. (S. 125-130).
@inproceedings{mci/Lamprecht2006,
author = {Lamprecht, Anna-Lena AND Margaria, Tiziana AND Steffen, Bernhard},
title = {Datenflussanalyse als Modelchecking im jABC},
booktitle = {Software Engineering 2006, Proceedings der Fachtagung des GI-Fachbereichs Softwaretechnik},
year = {2006},
editor = {Biel, Bettina AND Book, Matthias AND Gruhn, Volker} ,
pages = { 125-130 },
publisher = {Gesellschaft für Informatik e.V.},
address = {Bonn}
}
DateienGroesseFormatAnzeige
GI-Proceedings-79-14.pdf456.5Kb PDF Öffnen

Haben Sie fehlerhafte Angaben entdeckt? Sagen Sie uns Bescheid: Feedback abschicken

Mehr Information

ISBN: 3-88579-173-0
ISSN: 1617-5468
Datum: 2006
Sprache: de (de)
Typ: Text/Conference Paper
Sammlungen

Zur Langanzeige