Monitor synthesis for runtime checking of context-aware applications

OData support
Dr. Majzik István
Department of Measurement and Information Systems

The goal of this thesis to give a general solution for specifying requirements for context-aware systems and for the automatic runtime evaluation of them as well.

A graphical and a textual - temporal logic based - requirement specification language is being introduced in this paper. The graphical language is based on the UML Sequence Diagrams and the LSC scenario description language, while the textual language is an extended LTL formalism. Besides the precise and formal specification for both languages, this thesis includes the translation algorithm from the graphical notation to the textual language. Based on the requirements specified with the textual language, monitors can be synthesized automatically.

These monitors are able to verify weather the behavior of a running application satisfies or violates the given requirements. This thesis presents not just the general method of the monitor synthesis, but it also gives an overview of a proof of concept implementation, which is then analyzed with various measurements.

A crucial part of the work is the overview of the related works and the categorization of the already existing solutions. These summaries are always presented in the paper before defining the newly defined solutions.


Please sign in to download the files of this thesis.