Formal Analysis of Log Files

Runtime verification as a field faces several challenges. One key challenge is howto 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, it is shown 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. Although this approach prevents an online reaction to detected errors, possible with traditional runtime verification, it provides a powerful tool for test automation and debugging-in this case, analysis of spacecraft telemetry by ground operations teams at NASA's Jet Propulsion Laboratory. The second challenge is addressed in the presented work through a temporal specification language, designed in collaboration with Jet Propulsion Laboratory test engineers. The specification 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 rule-based language of the RULER runtime verification system. A case study is presented illustrating the use of our LOGSCOPE tool by software test engineers for the 2011 Mars Science Laboratory mission.