Transforming Timeline Specifications into Automata for Runtime Monitoring

Abstract. In runtime monitoring, a programmer specifies code to execute whenever a sequence of events occurs during program execution. Previous and related work has shown that runtime monitoring techniques can be useful in order to validate or guarantee the safety and security of running programs. Those techniques have however not been incorporated in everyday software development processes. One problem that hinders industry adoption is that the required specifications use a cumbersome, textual notation. As a consequence, only verification experts, not programmers, can understand what a given specification means and in particular, whether it is correct. In 2001, researchers at Bell Labs proposed the Timeline formalism. This formalism was designed with ease of use in mind, for the purpose of static verification (and not, as in our work, for runtime monitoring). In this article, we describe how software safety specifications can be described visually in the Timeline formalism and subsequ...

• Type: Conference
• Year: 2007
• Where: AGTIVE
• Authors: Eric Bodden, Hans Vangheluwe
• Keywords: AGTIVE 2007, Formal Methods, Runtime Monitoring, Runtime Monitoring Techniques, Runtime Monitors