Model-checking abstract state machines (2001) [pdf]

Abstract, state machines is one of oldest techniques for specifying, verifying, and implementing systems with high-confidence. The main advantage over most formal methods is they’re easy for average programmer to understand. Model-checking has similar benefit over full proving. I linked this paper to give people a taste since its intro uses Dining Philosopher’s problem while very clearly mapping it to the spec. Also shows temporal logics common in model-checking of distributed protocols and hardware.

People interested in applying something modern like this should check out Alloy Analyzer for easiest intro (w/ GUI), SPIN since it’s got more use in industry than anything, and B method (and/or RODIN toolkit) for refining ASM’s to real software. Latter was used in train control among other things. The link below under Applications will give you an idea of all the things the ASM model has been used for. Also, while looking for formal verification of them, I found a 1999 paper that showed a sequential, regular version was decidable while others were not to varying degrees. Sounded a lot like the decidable category (regular grammers?) the LANGSEC people promote these days but ASM folks doing it way sooner. Good modeling tools often as a side effect make good practices more obvious like that. ;)

https://web.eecs.umich.edu/gasm/