An entry point for formal methods: Specification and analysis of event logs

Howard Barringer, Alex Groce, Klaus Havelund, Margaret Smith

Research output: Contribution to journalConference articlepeer-review

4 Scopus citations


Formal specification languages have long languished, due to the grave scalability problems faced by complete verification methods. Runtime verification promises to use formal specifications to automate part of the more scalable art of testing, but has not been widely applied to real systems, and often falters due to the cost and complexity of instrumentation for online monitoring. In this paper we discuss work in progress to apply an event-based specification system to the logging mechanism of the Mars Science Laboratory mission at JPL. By focusing on log analysis, we exploit the “instrumentation” already implemented and required for communicating with the spacecraft. We argue that this work both shows a practical method for using formal specifications in testing and opens interesting research avenues, including a challenging specification learning problem.

Original languageEnglish (US)
Pages (from-to)16-21
Number of pages6
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
StatePublished - Mar 28 2010
Externally publishedYes
Event2009 FM-09 Workshop on Formal Methods for Aerospace, FMA 2009 - Eindhoven, Netherlands
Duration: Nov 3 2009 → …

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'An entry point for formal methods: Specification and analysis of event logs'. Together they form a unique fingerprint.

Cite this