@article {308, title = {Inferring Event Stream Abstractions}, journal = {Formal Methods in System Design}, year = {2018}, pages = {29}, chapter = {1}, abstract = {

We propose a formalism for specifying event stream abstractions for use in spacecraft telemetry processing. Our work is motivated by the need to quickly process streams with millions of events generated by the Curiosity rover on Mars. \ The approach builds a hierarchy of event abstractions for telemetry visualization and querying to aid human comprehension. \ Such abstractions can also be used as input to other runtime verification tools. Our notation is inspired by Allen\&$\#$39;s Temporal Logic, and provides a rule-based declarative way to express event abstractions. We present an algorithm for applying specifications to an event stream and explore modifications to improve the algorithm\&$\#$39;s asymptotic complexity. The system is implemented in both Scala and C, with the specification language implemented as internal as well as external DSLs. We illustrate the solution with several examples, a performance evaluation, and a real telemetry analysis scenario.

}, issn = {1572-8102}, doi = {10.1007/s10703-018-0317-z}, author = {Sean Kauffman and Klaus Havelund and Rajeev Joshi and Sebastian Fischmeister} }