Formal analysis of log files

Howard Barringer, Alex Groce, Klaus Havelund, Margaret Smith

Research output: Contribution to journalArticlepeer-review

71 Scopus citations


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 presentedwork 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 theRULER runtime verification system. A case study is presented illustrating the use of our LOGSCOPE tool by software test engineers for the 2011 Mars Science.

Original languageEnglish (US)
Pages (from-to)365-390
Number of pages26
JournalJournal of Aerospace Computing, Information and Communication
Issue number11
StatePublished - Nov 2010
Externally publishedYes

ASJC Scopus subject areas

  • Aerospace Engineering
  • Computer Science Applications
  • Electrical and Electronic Engineering


Dive into the research topics of 'Formal analysis of log files'. Together they form a unique fingerprint.

Cite this