Model-driven generation of runtime checks for system properties

Creating runtime monitors for interesting properties is an important research problem. Existing approaches to runtime verification require specifications that not only define the property to monitor, but also contain details of the implementation, sometimes even requiring the implementation to add special variables or methods for monitoring. Often intuitive properties such as “event X should only happen when objects A and B agree” have to be translated by developers into complex specifications, for example, pre- and post-conditions on several methods that only in concert express this simple property. In most specification languages, the result of this manual translation are specifications that are so strongly tailored to the program at hand and the objects involved that, even if the property occurs again in a similar program, the whole translation process has to be repeated to create a new specification. In this paper, we introduce the concept of property templates. Property templates are pre-defined constraints that can be easily reused in specifications. They are part of a model-driven framework that translates high-level specifications into runtime monitors specialized to the problem at hand. The framework is extensible: Developers can define property templates for constraints they often need and can specialize the code generation when the default implementation is not satisfactory. We demonstrate the use of the framework in some case studies using a set of functional and structural constraints that we developed through an extensive study of existing software specifications. The key innovations of the approach we present are three. First, the properties developed with this approach are reusable and apply to a wide range of software systems, rather than being ad hoc and tailored to one particular program. Second, the properties are defined at a relatively high level of abstraction, so that no detailed knowledge of the implementation is needed to decide whether a given property applies. Third, we separate the definition of precise assertions for properties, and the use of properties. That way, experts can determine which assertions are needed to assure properties, and other developers can easily use these definitions to annotate systems.