Skip to main content

Comprehension of Spacecraft Telemetry Using Hierarchical Specifications of Behavior

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8829))

Abstract

A key challenge in operating remote spacecraft is that ground operators must rely on the limited visibility available through spacecraft telemetry in order to assess spacecraft health and operational status. We describe a tool for processing spacecraft telemetry that allows ground operators to impose structure on received telemetry in order to achieve a better comprehension of system state. A key element of our approach is the design of a domain-specific language that allows operators to express models of expected system behavior using partial specifications. The language allows behavior specifications with data fields, similar to other recent runtime verification systems. What is notable about our approach is the ability to develop hierarchical specifications of behavior. The language is implemented as an internal DSL in the Scala programming language that synthesizes rules from patterns of specification behavior. The rules are automatically applied to received telemetry and the inferred behaviors are available to ground operators using a visualization interface that makes it easier to understand and track spacecraft state. We describe initial results from applying our tool to telemetry received from the Curiosity rover currently roving the surface of Mars, where the visualizations are being used to trend subsystem behaviors, in order to identify potential problems before they happen. However, the technology is completely general and can be applied to any system that generates telemetry such as event logs.

The work described in this publication was carried out at Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. D3 website, http://d3js.org

  2. Drools website, http://www.jboss.org/drools

  3. Mars Science Laboratory (MSL) mission website, http://mars.jpl.nasa.gov/msl

  4. Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittamplan, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: OOPSLA 2005, ACM Press (2005)

    Google Scholar 

  5. Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified event automata: Towards expressive and efficient runtime monitors. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 68–84. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Barringer, H., Havelund, K.: traceContract: A scala DSL for trace analysis. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 57–72. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Barringer, H., Rydeheard, D.E., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. J. Log. Comput. 20(3), 675–706 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  9. Basin, D.A., Klaedtke, F., Müller, S.: Policy monitoring in first-order temporal logic. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 1–18. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Bauer, A., Küster, J.-C., Vegliach, G.: From propositional to first-order monitoring. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 59–75. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  11. Bodden, E.: MOPBox: A library approach to runtime verification. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 365–369. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  12. Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 341–356. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  13. Forgy, C.: Rete: A fast algorithm for the many pattern/many object pattern match problem. Artificial Intelligence 19, 17–37 (1982)

    Article  Google Scholar 

  14. Goubault-Larrecq, J., Olivain, J.: A smell of orchids. In: Leucker, M. (ed.) RV 2008. LNCS, vol. 5289, pp. 1–20. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  15. Hallé, S., Villemaire, R.: Runtime enforcement of web service message contracts with data. IEEE Transactions on Services Computing 5(2), 192–206 (2012)

    Article  Google Scholar 

  16. Havelund, K.: Data automata in Scala. In: Leucker, M., Wang, J. (eds.) 8th International Symposium on Theoretical Aspects of Software Engineering, TASE 2014, Changsha, China, September 1-3. IEEE Computer Society Press, Los Alamitos (2014)

    Google Scholar 

  17. Havelund, K.: Rule-based runtime verification revisited. Software Tools for Technology Transfer (STTT) (April 2014); Published online

    Google Scholar 

  18. Luckham, D. (ed.): The Power of Events: An Introduction to Complex Event Processing in Distributed Enterprise Systems. Addison-Wesley (2002)

    Google Scholar 

  19. Meredith, P., Jin, D., Griffith, D., Chen, F., Roşu, G.: An overview of the MOP runtime verification framework. Software Tools for Technology Transfer (STTT) 14(3), 249–289 (2012)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Havelund, K., Joshi, R. (2014). Comprehension of Spacecraft Telemetry Using Hierarchical Specifications of Behavior. In: Merz, S., Pang, J. (eds) Formal Methods and Software Engineering. ICFEM 2014. Lecture Notes in Computer Science, vol 8829. Springer, Cham. https://doi.org/10.1007/978-3-319-11737-9_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-11737-9_13

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-11736-2

  • Online ISBN: 978-3-319-11737-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics