Choosing SAFM: We chose SAFM for several reasons:
- High criticality—it is capable of determining a safe landing trajectory for the shuttle autonomously in case of a failure requiring an abort during ascent;
- Commonality of interest with the developers and their willingness and availability to work with us;
- Good conformance of the application with technical criteria for C++ model checking using Propel; and
- Manageable size (approx. 30,000 LOC).