A Tutorial on Runtime Verification

Abstract. This tutorial presents an overview of the field referred as to runtime ver-ification. Runtime Verification is the study of algorithms, data structures, and tools focused on analyzing executions of systems. The performed analysis aims at im-proving the confidence in systems behavior, either by improving program under-standing, or by checking conformance to specifications or algorithms. This chapter focuses specifically on checking execution traces against requirements formalized in terms of monitors. It is first shown on examples how such monitors can be written using aspect-oriented programming, exemplified by ASPECTJ. Subsequently four monitoring systems are illustrated on the same examples. The systems cover such formalisms as regular expressions, temporal logics, state machines, and rule-based programming, as well as the distinction between external and internal DSLs