On combinations of static and dynamic analysis – Panel introduction

Abstract

Model checking [1] deals with the problem of deciding whether all runs of a system under scrutiny satisfy a given specification. As typically infinite runs of the system are of interest, a dynamic analysis of complete runs is not possible. Hence, model checking is necessarily a static analysis technique. Runtime verification [2] on the other hand concentrates on prefixes of runs of the system as it typically considers the actual, necessarily finite run of the system. So while both model checking and runtime verification focus on runs of the system under scrutiny they have a different focus and are applied on a different level of abstraction. In this presentation we elaborate on the similarities and differences of model checking and runtime verification, yet, we mainly introduce question but questions to be studied in the future. We recall the work pointed out in [3] putting runtime verification and (LTL-based) model checking into the same formal framework.