אחיה אליסף

In this paper we propose a novel approach to satellites-software development, that allows for modularity and formal verification, resulting with safe and robust satellite software. Specifically, we propose to use scenario-based programming where software components (modules) represent different aspects of mission scenarios and anti-scenarios (sequences of events that must not happen). We present examples of how specifications can be translated into code artifacts that represent them in a direct and intuitive way. We support this approach with a development environment that we are designing for creating an on-board mission software. Our environment includes an automatic model-checking tool for verifying the produced software and for bug detection. we show that verification can be done on specific parts of the model, on specific logical layers of the applications, and on the entire model at a specific abstraction level. This allows for modular design process, where modules are tested and verified as soon as their code is ready. Additionally, we describe a “hybrid laboratory” for advanced testing of the mission software. This laboratory uses a novel approach that allows for automatic generation of test scenarios, using scenario-based programming. We believe that... the development environment along with the hybrid laboratory, provide a viable solution for developing reliable satellite software.