Model Checking Techniques applied to Satellite Operational Mode Management