In reply to Chandler:
There’s no need to build a reference model of an FSM. You need to build a reference model of the requirements the FSM was designed for.
There are many tools out there that check the validity of the FSM (all states reachable, no deadlocks, etc) without you have to write any models.