S. Velder and A. Shalyto, “Verification of simple automata-based programs using the Model Checking method”, ICS, no. 3, pp. 27-38, Jun. 2007.