Formal Verification and Synthesis for an Air Traffic Management System