Abstract State Machines, Alloy, B, TLA, VDM, and Z - Yamine Ait Ameur, Klaus-Dieter Schewe (Springer Berlin Heidelberg, 2014)