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.