Automatic Generation of Executable Assertions for Runtime Checking Temporal Requirements

Checking various temporal requirements is a key dependability concern in safety-critical systems. As modelchecking 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 runtime 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 resourcerestricted embedded environments.

• Type: Conference
• Year: 2005
• Where: HASE
• Authors: Gergely Pintér, István Majzik
• Keywords: HASE 2005, Temporal Logic Formulae, Temporal Requirements, Various Temporal Requirements