Velder, S., Shalyto, A.: Verification of simple automata-based programs using the Model Checking method. Information and Control Systems(3), 27-38 (2007)