Curiosity: Monitoring Execution of Space Craft Flight Software

Here's the paper: http://www.havelund.com/Publications/logscope10.pdf

And a number of interesting articles citing it. http://goo.gl/LGZnT

A Few applications:

- Formally verifying programs not designed for formal verification. See for http://www.cs.man.ac.uk/~howard/Papers/ruler-tutorial.pdf example to instrument Java programs for runtime verification using AspectJ

- Using automata for log-analysis, immediately useful to any internet company with large amounts of logs, imagine an automata DSL to analyze data flows from Flume/Scribe into Hadoop