Let’s Look at the Logs: Low-Impact Runtime Verification∗
Alex Groce, Klaus Havelund, Margaret Smith, Howard Barringer · 2009
Runtime verification as a field faces several challenges. One key challenge is how to keep the overheads associated with its application low. This is especially important in real-time critical embedded applications, where memory and CPU resources are limited. Another challenge is that of devising expressive and yet user-friendly specification languages that can attract software engineers. In this paper, we show that for many systems, in-place logging provides a satisfactory basis for postmortem “runtime” verification of logs, where the overhead is already included in system design. While this approach prevents on-line reaction to detected errors, possible with traditional runtime verification, it provides a powerful tool for test automation and debugging — in our case, analysis of spacecraft telemetry by ground operations teams at NASA’s Jet Propulsion Laboratory (JPL). The second challenge is addressed in the presented work through a temporal pattern language, designed in collaboration with JPL test engineers. The pattern language allows for descriptions of relationships between data-rich events (records) common in logs, and is translated into a form of automata supporting data parameterized states. The automaton language is inspired by the rulebased language of the RULER runtime verification system. We present a case study illustrating the use of our LOGSCOPE tool by software test engineers for the 2011 Mars Science Laboratory mission.