Symbolic Refinement of Extended State Machines with Applications to the Automatic Derivation of Sub-Components and Controllers