TITLE:
Refinement in Formal Proof of Equivalence in Morphisms over Strongly Connected Algebraic Automata
AUTHORS:
Nazir Ahmad Zafar, Ajmal Hussain, Amir Ali
KEYWORDS:
Formal Methods, Automata, Integration of Approaches, Z Notation, Validation
JOURNAL NAME:
Journal of Software Engineering and Applications,
Vol.2 No.2,
July
15,
2009
ABSTRACT: Automata theory has played an important role in computer science and engineering particularly modeling behavior of systems since last couple of decades. The algebraic automaton has emerged with several modern applications, for ex-ample, optimization of programs, design of model checkers, development of theorem provers because of having proper-ties and structures from algebraic theory of mathematics. Design of a complex system not only requires functionality but it also needs to model its control behavior. Z notation is an ideal one used for describing state space of a system and then defining operations over it. Consequently, an integration of algebraic automata and Z will be an effective computer tool which can be used for modeling of complex systems. In this paper, we have combined algebraic automata and Z notation defining a relationship between fundamentals of these approaches. At first, we have described algebraic automaton and its extended forms. Then homomorphism and its variants over strongly connected automata are speci-fied. Finally, monoid endomorphisms and group automorphisms are formalized, and formal proof of their equivalence is given under certain assumptions. The specification is analyzed and validated using Z/EVES tool.