In this paper, we use a case study from an autonomous aerospace context as running example to show how to apply a game-based model-checking approach a as a powerful technique for the verification, diagnosis and adaptation of temporal properties. This work is part of our contribution within the SHADOWS project, where we provide a number of enabling technologies for model-driven self-healing. We propose here to use GEAR, a game-based model checker for the full modal μ-calculus and derived, more user-oriented logics, as a user friendly tool that can offer automatic proofs of critical properties of such systems. Designers and engineers can interactively investigate automatically generated winning strategies for the games, this way exploring the connection between the property, the system, and the proof.