"Be careful with not generating specs and models with state spaces too big that make model checking impossible."
Yes, I come from an engineering background, as in electrical, automation and functional safety, and been using state machines in a practical way for many years - there are a few techniques to lessen the size of any given FSM, the first one being if you can break out a conditioning FSM to manage mode (eg Local. Off, Auto, Remote is a common circumstance in process plant, or similar for machinery.)
Then there is the system and subsystem breakdown concept, a trivial example being do you do an FSM for one motor that can run forward or reverse as a single FSM, or do you have an FSM that is for a motor that only runs in one direction, and interconnect two of them for a reversing motor - because forward and reverse are mutually exclusive that is potentially better as two machines, even though it is one object. Do this and break out even just local/remote as well and you can be up to one sixteenth the number of states (more or less) straight away. Big difference.
Then at a larger scale sometimes you might build layers of hierarchy, with one to many and many to one FSM intermediaries between the layers, that do not directly relate to any real world objects - synthetic FSM for convenience.
You can also have nested FSM, where a transition might be dependant on the result of an FSM sub-system, it's like a subroutine - sometimes useful for more batching like applications where you might have an optional detour via a subsequence, for warm-up or cleaning, that might not always be done, eg just first batch run of the day, or when cold.
And so on, many small tricks I have evolved over the years for practical use.
I find that the black art is the optimal system and subsystem decomposition. It is hard to teach and is best learned by trying and failing a little, like learning to ride a bike.
Gareth