(Universidad Abierta Interamericana. Facultad de Tecnología Informática, 2023-6-30)
Asteasuain, Fernando
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).