Automatic Generation of Executable Assertions for Runtime Checking Temporal Requirements

Checking various temporal requirements is a key dependability concern in safety-critical systems. As model-checking approaches do not scale well to systems of high complexity the runtime verification of temporal requirements has received a growing attention recently. This paper presents a code-generation based method for run-time evaluation of linear temporal logic formulae over program execution traces. The processing-power requirements of our solution are much lower than in case of previous approaches enabling its application even in resource-restricted embedded environments.