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 analyse these temporal behaviours. Various approaches exist in the literature supporting the definition of temporal behaviours, and many of them are defined based on automata theory. Automata are usually easier to analyse algorithmically as the accepted languages of these automata can be formally analysed.

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 temporal behavior is examined. The solution is analysed in terms of expressiveness, and a mapping from a high level domain specific language to this automata representation is introduced.


Please sign in to download the files of this thesis.