Expectations of Formal Model Analysis Methods: Implications for SIG-MA