文章基本信息

标题：Refinement in Formal Proof of Equivalence in Morphisms over Strongly Connected Algebraic Automata
本地全文：下载
作者：Nazir Ahmad Zafar ; Ajmal Hussain ; Amir Ali 等
期刊名称：Journal of Software Engineering and Applications
印刷版ISSN：1945-3116
电子版ISSN：1945-3124
出版年度：2009
卷号：2
期号：2
页码：77-85
DOI：10.4236/jsea.2009.22012
出版社：Scientific Research Publishing
摘要：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.
关键词：Formal Methods; Automata; Integration of Approaches; Z Notation; Validation