Formal Validation of Software for Nano Satellite Missions

Fernando Asteasuain

doi:10.59471/raia202353

Autores/as

Fernando Asteasuain Universidad Nacional de Avellaneda, Buenos Aires, Argentina.

DOI:

https://doi.org/10.59471/raia202353

Palabras clave:

Nano satélites, verificación formal, síntesis de comportamiento

Resumen

Space research industry has become one of the most successful domains in the last years. In particular, the development of nano satellites has emerged as a stunning field since its low costs of production. The software in charge of the satellite functioning must be carefully verified to check that system fulfills the expected behavior. In this work we provide a full, complete and declarative framework to formally validate software for nano satellite missions, including behavioral synthesis which is a distinguishable contribution in this field. When validating the satellite behavior we include requirements from different sources: on board computer, IoT protocols, operating system and mission properties. Our framework is based on the declarative and graphical language FVS (Feather Weight Visual Scenarios).

Métricas

Cargando métricas ...

Citas

» [1] Déharbe, D., Galvao, S., & Moreira, A. M. (2009, August). Formalizing freertos: First steps. In Brazilian Symposium on Formal Methods (pp. 101-117). Springer, Berlin, Heidelberg.

» [2] Saeed, N., Elzanaty, A., Almorad, H., Dahrouj, H., Al-Naffouri, T. Y., & Alouini, M. S. (2020). Cubesat communications: Recent advances and future challenges. IEEE Communications Surveys & Tutorials, 22(3), 1839-1862.

» [3] Hanafi, A., Derouich, A., Karim, M., & Lemmassi, A. (2021, January). Design and Implementation of an Open Source and Low-Cost Nanosatellite Platform. In International Conference on Digital Technologies and Applications (pp. 421-432). Springer, Cham.

» [4] Williams, C. and DelPozzo S. Nano Microsatellite Market Forecast - 10th Edition, Space-Works Annual Nano/Microsatellite Market Assessment, 2020.

» [5] Krishnan, R., & Lalithambika, V. R. (2020). Modeling and Validating Launch Vehicle Onboard Software Using the SPIN Model Checker. Journal of Aerospace Information Systems, 17(12), 695-699.

» [6] Aurandt, A., Jones, P. H., & Rozier, K. Y. (2022). Runtime verification triggers real-time, autonomous fault recovery on the CySat-I. In NASA Formal Methods Symposium (pp. 816-825). Springer, Cham.

» [7] Tipaldi, M., Legendre, C., Koopmann, O., Ferraguto, M., Wenker, R., & D’Angelo, G. (2018). Development strategies for the satellite flight software on-board Meteosat Third Generation. Acta Astronautica, 145, 482-491.

» [8] Wenker, R., Legendre, C., Ferraguto, M., Tipaldi, M., Wortmann, A., Moellmann, C., & Rosskamp, D. (2017, June). On-board software architecture in MTG satellite. In 2017 IEEE International Workshop on Metrology for AeroSpace (MetroAeroSpace) (pp. 318-323). IEEE.

» [9] Pressman, A. (2019). Why Facebook, SpaceX and dozens of others are battling over Internet access from space. Fortune.

» [10] Kulu E.. “Nanosatellite and cubesat database,” 2019. [Online]. Available: https://www.nanosats.eu/

» [11] Alam, M., Khamees, A., Aboelnaga, T., Amer, A., Harbi, A., Alamir, M., ... & Elsayed, O. A. (2021, August). Design and Implementation of an Onboard Computer and payload for Nano Satellite (CubeSat). In The International Undergraduate Research Conference (Vol. 5, No. 5, pp. 361-364). The Military Technical College.

» [12] D’Ippolito, N. R., Braberman, V., Piterman, N., & Uchitel, S. (2010, November). Synthesis of live behaviour models. In Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineering (pp. 77-86).

» [13] Asteasuain F. (2021). “Formalizing Operating Systems for nano satellites On Board Computers”. 10mo. Congreso Nacional de Ingeniería Informática y Sistemas de Información CoNaIISI 2022.

» [14] Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N.Wu, and W.-C. Chan. Goal: A graphical tool for manipulating büchi automata and temporal formulae. In TACAS, pages 466-471. Springer, 2007

» [15] Uchitel, S., Chatley, R., Kramer, J., & Magee, J. (2003, April). LTSA-MSC: Tool support for behaviour model elaboration using implied scenarios. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 597-601). Springer, Berlin, Heidelberg.

» [16] Asteasuain, F. , Braberman, V. (2017). Declaratively building behavior by means of scenario clauses. Requirements Engineering, 22(2), 239-274.

» [17] Asteasuain, F, Calonge F, Dubinsky M, . Gamboa P. Open and branching behavioral synthesis with scenario clauses. CLEI ELECTRONIC JOURNAL, 24(3), 2021.

» [18] Asteasuain F. (2021). “Controller Synthesis for IoT Protocols Verification”. 9no. Congreso Nacional de Ingeniería Informática y Sistemas de Información CoNaIISI 2021. Modalidad Virtual. Facultad Regional Mendoza. Universidad Tecnológica Nacional. Mendoza, 4 y 5 de Noviembre de 2021.

» [19] Maoz S. and Ringert J. O.. Synthesizing a lego forklift controller in gr (1): A case study. arXiv preprint arXiv:1602.01172, 2016.

» [20] Dwyer, M. Avrunin, M, and Corbett M.. Patterns in property specifications for finite-state verification. In ICSE, pages 411-420, 1999.

» [21] Tressler, J. F., Alkoy, S., & Newnham, R. E. (1998). Piezoelectric sensors and sensor materials. Journal of electroceramics, 2, 257-272.

» [22] Cruz-Camacho, E., Amer, A., Kopsaftopoulos, F., & Varela, C. A. (2023). Formal Safety Envelopes for Provably Accurate State Classification by Data-Driven Flight Models. Journal of Aerospace Information Systems, 20(1), 3-16.

» [23] Jackson, J., Laurenti, L., Frew, E., & Lahijanian, M. (2020, December). Safety verification of unknown dynamical systems via gaussian process regression. In 2020 59th IEEE Conference on Decision and Control (CDC) (pp. 860-866). IEEE.

» [24] Jeannin, J. B., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., & Platzer, A. (2015). A formally verified hybrid system for the next-generation airborne collision avoidance system. In Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 21 (pp. 21-36). Springer Berlin Heidelberg.

» [25] Paul, S., Kopsaftopoulos, F., Patterson, S., & Varela, C. A. (2020). Towards Formal Correctness Envelopes for Dynamic Data-Driven Aerospace Systems. Handbook of Dynamic Data-Driven Application Systems, edited by Darema F. and Blasch E., Springer, Berlin.