|
Title
|
|
|
|
Transforming timeline specifications into automata for runtime monitoring
| |
|
Author
|
|
|
|
| |
|
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 subsequently transformed into finite automata suitable for runtime monitoring, using our meta-modelling and model transformation tool AToM3. The synthesized automata are subsequently fed into an existing monitoring back-end that generates efficient runtime monitors for them. Those monitors can then automatically be applied to Java programs. Our work shows that the transformation of Timeline models to automata is not only feasible in an efficient and sound way but also helps programmers identify correspondences between the original specification and the generated monitors. We argue that visual specification of safety criteria and subsequent automatic synthesis of runtime monitors will help users reason about the correctness of their specifications on the one hand and effectively deploy them in industrial settings on the other hand. |
| |
|
Language
|
|
|
|
English
| |
|
Source (journal)
|
|
|
|
Lecture notes in computer science. - Berlin, 1973, currens
| |
|
Publication
|
|
|
|
Berlin
:
2008
| |
|
ISSN
|
|
|
|
0302-9743
[print]
1611-3349
[online]
| |
|
DOI
|
|
|
|
10.1007/978-3-540-89020-1_18
| |
|
Volume/pages
|
|
|
|
5088
(2008)
, p. 249-264
| |
|
ISI
|
|
|
|
000262477700018
| |
|
Full text (Publisher's DOI)
|
|
|
|
| |
|