Abstract State Machines, Alloy, B, TLA, VDM, and Z - Butler (Springer International Publishing, 2018)