Elicitation and formal specification of run time assurance requirements for aerospace collision avoidance systems