[petra]

On the other hand, hierarchical-state-machine (like FSM, with hierarchy), are often used in embedded systems(including safety-critical systems) and are considered among the more reliable and bug-free methodologies.

So maybe we shouldn't rule-out FSM's but be subtle in their use ?

[AstralStorm]

Better still, why not use maths and convert FSM into mathematical proofs? It is automatic if the FSM is fully specified and the semi-automatic part could catch insufficient specification. (to borrow words from reply above: certain kinds of implicit state and assumptions on the platform)

Something like Isabelle/HOL etc.