A declarative and probabilistic model with rewards to formally verify satellite missions

Abstract

Software Probabilistic models can be extended with the concept of rewards to enrich and enhance the behavioral properties to be specified and studied in a software system. In the last years, rewarded probabilistic models have been employed to formally verify cutting-edge domains such as satellite missions specifications. In this work we present an extension of our flexible and graphical specification framework called FVS incorporating rewards into our probabilistic model. We validated our approach by modeling a real and complex case of study for a nanosatellite and we also developed an important software tool to simulate satellite missions and recollect data