N.A. Zafar, A. Hussain, and A. Ali (Pakistan)
Integration of approaches, Algebraic automata, Formal methods, Z notation, Validation
Automata theory has been a cornerstone of theoretical computer science since last fifty years. The algebraic automaton has emerged with several modern applications. Design of a complex system not only requires functionality but also needs to capture its control behavior. Automata theory is powerful in modeling behaviour while Z notation is an ideal specification language used for describing state space of a system. Consequently, an integration of automata and Z will be a useful tool for modeling of complex systems. In this paper, we have identified and established a relationship between fundamentals of automata and Z structures. Initially, we have described formal specification of the extended algebraic automata then the sub automaton operator is described. Formal definition of algebraic automaton is then extended to cyclic automaton. Finally, the cross product of two automata is formalized and its strong connectedness is checked. The formal specification is analyzed and validated using Z/EVES tool.
Important Links:
Go Back
