Validación Formal de Software para misiones de nano satélites

Resumen

La industria aeroespacial representa uno de las áreas de mayor crecimiento y éxito de los últimos años. En particular, el desarrollo de los denominados nanos satélites se ha destacado por sus bajos costos de producción. El software encargado de monitorear y ejecutar las tareas del satélite debe ser formalmente verificado para asegurar su correcto funcionamiento. En este trabajo proponemos un framework completo, íntegro y declarativo para verificar formalmente el comportamiento de nano satélites, incluyendo la síntesis de comportamiento, que es una contribución valiosa y poco explorada en este dominio. Para la experimentación tomamos requerimientos de diferentes lugares como la computadora de a bordo, los protocolos de IoT de comunicación, requerimientos del sistema operativo y también de la propia misión satelital. Nuestro framework se basa en el lenguaje de especificación gráfico y declarativo denominado FVS (Feather Weight Visual Scenarios)