Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry

Elucidation and Analysis of Specification Patterns
in Aerospace System Telemetry

Zachary Luppen, Michael Jacks, Nathan Baughman, Muhamed Stilic, Ryan Nasers, Benjamin Hertz, James Cutler, Dae-Young Lee, and Kristin Yvonne Rozier

This webpage contains research artifacts from "Elucidation and Analysis of Specification Patterns
in Aerospace System Telemetry" by Z. Luppen, M. Jacks, N. Baughman, M. Stilic, R. Nasers, B. Hertz, J. W. Cutler, D. Y. Lee, K. Y. Rozier

List of all References

1. AeroVironment, I.: Vapor uas: Helicopter drone with drop delivery (2021), "https://www.avinc.com/uas/vapor"

2. Aurandt, A., Jones, P., Rozier, K.Y.: Runtime Verification Triggers Real-time, Autonomous Fault Recovery on the CySat-I. In: Proceedings of the 14th NASA Formal Methods Symposium (NFM 2022). Springer, Caltech, California, USA (May 2022)

3. Balloonnews, Balloonnews: 10 ways that a high altitude balloon flight can go wrong (Aug 2014), https://balloonnews.wordpress.com/2014/04/10/10-ways-that-a-high-altitude-balloon-flight-can-go-wrong/

4. Basta, T., Miller, S., Clark, R.T.: Weather Balloon Altitude Control System. Montana State University (2014-2015)

5. Cauwels, M., Hammer, A., Hertz, B., Jones, P., Rozier, K.: Integrating Runtime Verifica- tion into an Automated UAS Traffic Management System, pp. 340–357. Springer, Cham (09 2020). https://doi.org/10.1007/978-3-030-59155-7

6. ESRA Board of Directors: 2019 spaceport america cup (2019), http://www.soundingrocket.org/2019-sa-cup.html

7. Fisher, M., Mascardi, V., Rozier, K.Y., Schlingloff, B.H., Winikoff, M., Yorke-Smith, N.:Towards a framework for certification of reliable autonomous systems. Autonomous Agents and Multi-Agent Systems 35 (04 2021). https://doi.org/10.1007/s10458-020-09487-2

8. Garg, K.: Autonomous Navigation System for High Altitude Balloons. Ph.D. thesis, Lule ̊a Technical University, Graphic Production 2019 (2019)

9. Geist, J., Rozier, K.Y., Schumann, J.: Runtime Observer Pairs and Bayesian Network Rea- soners On-board FPGAs: Flight-Certifiable System Health Management for Embedded Sys- tems. In: Proceedings of the 14th International Conference on Runtime Verification (RV14). vol. 8734, pp. 215–230. Springer-Verlag (September 2014)

10. Hammer, A., Cauwels, M., Hertz, B., Jones, P., Rozier, K.Y.: Integrating runtime verifica- tion into an automated uas traffic management system. Innovations in Systems and Software Engineering: A NASA Journal (July 2021). https://doi.org/10.1007/s11334-021-00407-5

11. Hertz, B., Luppen, Z., Rozier, K.Y.: Integrating runtime verification into a sounding rocket control system. In: Dutle, A., Moscato, M.M., Titolo, L., Mu ̃noz, C.A., Perez, I. (eds.) NASA Formal Methods. pp. 151–159. Springer International Publishing, Cham (2021)

12. Kempa, B., Zhang, P., Jones, P.H., Zambreno, J., Rozier, K.Y.: Embedding Online Run- time Verification for Fault Disambiguation on Robonaut2. In: Proceedings of the 18th In- ternational Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science (LNCS), vol. TBD, p. TBD. Springer, Vienna, Austria (September 2020). https://doi.org/TBD, http://research.temporallogic.org/papers/KZJZR20.pdf

13. eXploration Lab, T.M.: Grifex (2021), https://exploration.engin.umich.edu/blog/?page id=2684

14. Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for Mission-time LTL. In: Proceedings of 31st International Conference on Computer Aided Verification (CAV). LNCS, vol. 11562, pp. 3–22. Springer, New York, NY, USA (July 2019). https://doi.org/https://doi.org/10.1007/978-3-030-25543-5

15. Luppen, Z., Jacks, M., Baughman, N., Stilic, M., Nasers, R., Lee, D.Y., Rozier, K.Y., Cutler, J.: Runtime verification of the dynamic performance degradation of the grifex cubesat (under review). In: NASA Formal Methods. Springer International Publishing (2022)

16. Luppen, Z.A., Lee, D.Y., Rozier, K.Y.: A case study in formal specification and runtime verification of a CubeSat communications system. In: AIAA Scitech 2021 Forum. American Institute of Aeronautics and Astronautics (Jan 2021). https://doi.org/10.2514/6.2021-0997, https://doi.org/10.2514/6.2021-0997

17. M2I: Make to innovate (m:2:i) (2021), https://m2i.aere.iastate.edu/

18. M2I: Project goals (habet) (2021), https://m2i.aere.iastate.edu/habet/project-goals-and-scope-of-work/

19. Marshall, R.: Cutdown mechanisms (Mar 2021), https://sites.google.com/site/ki4mcw/Home/cutdown-mechanisms

20. Merkert, R., Bushell, J.: Managing the drone revolution: A systematic literature re- view into the current use of airborne drones and future strategic directions for their effective control. Journal of Air Transport Management 89, 101929 (Oct 2020). https://doi.org/10.1016/j.jairtraman.2020.101929, https://doi.org/10.1016/j.jairtraman.2020.101929

21. Meyer, J.J., Flaten, J.A., Candler, G.V.: Pdf (Apr 2021)

22. Mike Tolmasoff, Renelito Delos Santos, and Catherine Venturini: Improving mission success of cubesats. In: Proceedings of the U.S. Space Program Mission Assurance Improvement Workshop (May 2007)

23. Moosbrugger, P., Rozier, K.Y., Schumann, J.: R2U2: Monitoring and Diagnosis of Security Threats for Unmanned Aerial Systems. Formal Methods in System Design pp. 1–31 (April 2017). https://doi.org/10.1007/s10703-017-0275-x 10 Z. Luppen et al.

24. NASA CubeSat Launch Initiative: CubeSat 101. California Polytechnic State University, San Luis Obispo (Cal Poly) CubeSat Systems Engineer Lab, 1 edn. (2017)

25. Papp, D.: Archery release becomes reusable balloon cutdown mechanism (Mar 2021), https://hackaday.com/2021/03/27/archery-release-becomes-reusable-balloon-cutdown-mechanism/

26. Phillips, T., Johnson, S., Koske-Phillips, A., White, M., Yarborough, A., Lamb, A., Herbst, A., Molina, F., Gilpin, J., Grah, O., Perez, G., Reid, C., Harvey, J., Schultz, J.: Space weather ballooning. Space Weather 14(10), 697–703 (2016). https://doi.org/https://doi.org/10.1002/2016SW001410, https://agupubs.onlinelibrary.wiley.com/doi/abs/10.1002/2016SW001410

27. Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Proceedings of the 20th Interna- tional Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science (LNCS), vol. 8413, pp. 357–372. Springer-Verlag (April 2014)

28. Rozier, K.Y., Schumann, J., Ippolito, C.: Intelligent Hardware-Enabled Sensor and Software Safety and Health Management for Autonomous UAS. Technical Memorandum NASA/TM- 2015-218817, NASA, NASA Ames Research Center, Moffett Field, CA 94035, USA (May 2015)

29. Rozier, K.Y.: Specification: The biggest bottleneck in formal methods and autonomy. In: Proceedings of 8th Working Conference on Verified Software: Theories, Tools, and Exper- iments (VSTTE 2016). LNCS, vol. 9971, pp. 1–19. Springer-Verlag, Toronto, ON, Canada (July 2016). https://doi.org/10.1007/978-3-319-48869-1

30. Schumann, J., Moosbrugger, P., Rozier, K.Y.: R2U2: Monitoring and Diagnosis of Security Threats for Unmanned Aerial Systems. In: Proceedings of the 15th International Conference on Runtime Verification (RV15). Springer-Verlag, Vienna, Austria (September 2015)

31. Schumann, J., Moosbrugger, P., Rozier, K.Y.: Runtime Analysis with R2U2: A Tool Exhi- bition Report. In: Proceedings of the 16th International Conference on Runtime Verification (RV16). Springer-Verlag, Madrid, Spain (September 2016)

32. Schumann, J., Rozier, K.Y., Reinbacher, T., Mengshoel, O.J., Mbaya, T., Ippolito, C.: To- wards real-time, on-board, hardware-supported sensor and software health management for unmanned aerial systems. International Journal of Prognostics and Health Management (IJPHM) 6(1), 1–27 (June 2015)

33. Science, H.A.: Intro to weather balloons (2021), https://www.highaltitudescience.com/pages/intro-to-weather-balloons

34. Seibert, G.: The history of sounding rockets and their contribution to european space re- search. ESA History Study Reports (11 2006)

35. Wong, K.: Nasa’s deuce-carrying rocket fails to collect data due to technical glitch (Nov 2017), https://www.aerospace-technology.com/news/newsnasas-deuce-carrying-rocket-fails-to-collect-data-due-to-technical-glitch-5962942