An Automated Verification System for Finite State Machines

This paper describes an automated verification system that checks if an input finite state machine satisfies specifications for them. The finite state machine is represented in the FSM language, while specifications are represented in a language derived from a temporal logic. The verification system reports how verifications proceed and, in case of failure, why the machine fails to satisfy the specification.