Synchronous model of automaton program

Abstract

This article presents a model of automaton program that satisfies synchronous model requirements. A formal automaton program model lets to use an existing technologies and tools of synchronous programs verification for checking automaton programs. An Esterel language and an Esterel Technologies Inc. toolbox will be used to build a program verifier.