Construction of Morphisms over Extended Algebraic Automata Using Z
Nazir Ahmad Zafar, Ajmal Hussain, Amir Ali · 2008
Algebraic automaton has emerged with several modern applications in computer science and engineering. Design of theorem provers, development of model checkers, optimization of programs are some of its applications. The Z notation is suitable for modeling static while automata are powerful for describing dynamic parts of a system. Consequently, their integration is required. In this paper, we have proposed a relationship between the fundamentals of algebraic automata and Z. Initially, we have given formalization of the extended algebraic automata.Then formal construction of homomorphism is described and extended to isomorphism. Finally, a formal procedure of conversion from homomorphism (isomorphism) to endomorphism (automorphism) is given. The formal specification is analyzed and validated using Z/EVES tool.