Abstract:
This article presents a synchronous model of the automaton program. A technique of verification of synchronous-automaton programs has been developed. Some properties of the model are checked automatically. There is an ability of verifying user-defined properties. This technique helps to discover errors often made during the design process.