Applicability of Integrating Automata and Z: A Case Study

System specification and functionality are primary requirements in modeling and design of complex and automated systems. Z notation is a powerful language used for specification. Automata theory is a graph-based tool for modeling and capturing behavior of automated systems. In this paper, an effective combination of the two approaches is presented to propose a novel integrated approach. The integration will help to program the automata for verification of systems. A case study of vending machine is taken to evaluate the proposed approach. First of all, abstract formal specification of Deterministic Finite Automata is presented. Then an automaton of vending machine is described. A linkage between abstract model of automata and real study of vending machine is investigated. A string accepter in automata helps to describe "buying the product" operation in the vending machine. The language accepter in automata is mapped with the complete functional machine. The specification is described using Z notation and analyzed using Z/Eves tool.