And once you're confortable with FSM's, you might try Abstract, State Machines (ASM's) for formally specifying or verifying software: http://www.di.unipi.it/~b

And once you're confortable with FSM's, you might try Abstract, State Machines (ASM's) for formally specifying or verifying software: http://www.di.unipi.it/~boerger/Papers/Methodology/BcsFacs07.pdf http://www.di.unipi.it/~boerger/Papers/Methodology/BcsFacs07... Microsoft even had a gool, AsmL, for this method. TLA's PlusCal specs look similar to some Ive seen in ASM's, too.