The size and complexity of software in spacecraft is increasing exponentially and this trend complicates its validation within the context of the overall spacecraft system. Current validation methods are labor-intensive as they rely on manual analysis, review and inspection. That is why we developed - with requirements from the European space industry - a novel modeling language and toolset for a (semi-)automated validation approach. Our modeling language is a dialect of the Architecture Analysis and Design Language (AADL) and enables engineers to express the spacecraft system design, the software design, and their reliability aspects in a single integrated model. The model can subsequently be analyzed by the COMPASS toolset. This toolset utilizes state-of-the-art model checking techniques, both qualitative and probabilistic, for checking requirements related to functional correctness, safety & dependability and performance. Several studies using satellite design data have been performed by industry. We report on them in this chapter. The formal nature of our approach enables engineers to identify, evaluate and address intricate strengths and weaknesses in the system software architecture through rigorous and automated methods. Our experience report on these methods with our satellite cases can be used to kickstart future formal model-based validation efforts.