Implementierung einer Monitorkonstruktion für sichtbar-kontextfreie Eigenschaften

RVLib ist ein Java-Framework zur Lufzeitüberwachung von Bytecode-Programmen für die Java Virtual Machine. Es bildet unter anderem die Basis für jUnitRV. Laufzeiteigenschaften können in verschiedenen Formalismen spezifiziert werden, z.B. LTL. Jeder formalisum bietet eigene Vorteile aber auch Einschränkungen. So lassen sich viele zeitliche Eigenschaften z.B. in LTL gut darstellen. Jedoch können in LTL nicht alle regulären Eigenschaften formuliert werden (sondern nur „sternfreie“ Eigenschaften). Klammerstrukturen sind nicht einmal mehr regulär (sondern echt kontextfrei) aber, besonders in gegenwart von verschachtelten Funktionsaufrufen (call stack), wichtig. Da kontextfreie Eigenschaften z.B. nicht unter Schnitt abgeschlossen sind (d.h. eine „Verundung“ ist nicht allgemein möglich), ist die Klasse der sichtbar-kontextfreien (visibly context free) Eigenschaften interessant, die viele übliche Operationen (wie Schnitt, Komplementierung) erlaubt.

Wesentlicher Bestandteil von RVLib ist die generierung der Überwachungslogik aus einer Spezifikation, die sog. Monitorsynthese. In dieser Arbeit soll eine Monitorsynthese aus sichbar-kontextfreien Eigenschaften implementiert werden. Die theoretischen Grundlagen dazu müssen nicht entwickelt, aber für eine erfolgreiche Implementierung in gewissem Umfang nachvollzogen werden.

Literatur

Runtime Verification und Monitorsynthese

• Normann Decker, Martin Leucker, Daniel Thoma: Impartiality and Anticipation for Monitoring of Visibly Context-free Properties. In A. Legay and S. Bensalem (Eds.): International Conference on Runtime Verification, RV 2013, LNCS 8174. Springer (2013)
• Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5) (2009) 293–303
• Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In Sokolsky, O., Tasiran, S., eds.: RV. Volume 4839 of Lecture Notes in Computer Science., Springer (2007) 126–138

Visibly Pushdown Automata

• Alur, R., Madhusudan, P.: Visibly pushdown languages. In Babai, L., ed.: STOC, ACM (2004) 202–211