Complex event processing based on automata theory

OData support
Dr. Vörös András
Department of Measurement and Information Systems

In traditional safety-critical systems, runtime verification is a frequently used

method. The goal of runtime verification is to synthesize verification components, which

can detect the possible failures of the components. Over the last few years, researchers

of my department have started developing a framework called VIATRA-CEP being able

to support the runtime analysis and verification of complex systems. This framework

uses live models, and defines the temporal expressions by model transformation rules

over these live models. Verification of model transformations are generally algorithmically undecidable therefore it is hard to analyze these temporal behaviors.

Various approaches exist in the literature supporting the definition of temporal behaviors, and many of them are defined based on automata theory.

Automata are usually easier to analyze algorithmically as the accepted languages of these automata can be formally analyzed.

In this thesis various automata based property representations are overviewed,

and a possible extension of the VIATRA-CEP framework is outlined. An automata

representation implementation for the analysis of parametric and temporal behavior is examined. The

solution is analyzed in terms of expressiveness, and a mapping from a high level domain

specific language to this automata representation is introduced.

An automaton executor implementation is also overviewed, alongside with the data structures which are required for the parametric timed execution.


Please sign in to download the files of this thesis.