53 25 v 3 [ cs . F L ] 2 0 Ja n 20 15 Runtime Verification Based on Register Automata

We propose TOPL automata as a new method for runtime verificat ion of systems with unbounded resource generation. Paradigmat ic such systems are object-oriented programs which can dynamically generate a n unbounded number of fresh object identities during their execution. Our f ormalism is based on register automata, a particularly successful approach in a utomata over infinite alphabets which administers a finite-state machine with bou ndedly many inputstoring registers. We show that TOPL automata are equally ex pressive to register automata and yet suitable to express properties of programs . Compared to other runtime verification methods, our technique can handle a cla ss of properties beyond the reach of current tools. We show in particular that pr ope ties which require value updates are not expressible with current techni ques yet are naturally captured by TOPL machines. On the practical side, we present a tool for runtime verification of Java programs via TOPL properties, where the trade-off between the coverage and the overhead of the monitoring system is tun able by means of a number of parameters. We validate our technique by checking properties involving multiple objects and chaining of values on large open sou rce projects.