Visual specification languages
In general, my research is concerned with making runtime verification more accessible. One crucial part in the tool chain has to be the support for easily denoting specifications, which can then later on be checked using runtime verification tools, such as J-LO or tracematches. In my AGTIVE 07 paper, I investigated the Timeline formalism, as visual specification formalism for temporal safety properties and how it could be translated into finite state machines for runtime monitoring. For that purpose we used the visual modeling environment AToM3, which allowed us to implement the entire semantics via a visual graph transformation.
Timeline was not developed by myself but rather had been proposed by Margaret H. Smith, Gerard J. Holzmann and Kousha Etessami from Bell Labs in 2001.
