African Journal of
Mathematics and Computer Science Research

  • Abbreviation: Afr. J. Math. Comput. Sci. Res.
  • Language: English
  • ISSN: 2006-9731
  • DOI: 10.5897/AJMCSR
  • Start Year: 2008
  • Published Articles: 248

Full Length Research Paper

Formal partitioning analysis and verification of extended algebraic automata

Nazir Ahmad Zafar
Department of Computer Science, King Faisal University, Hofuf, Saudi Arabia.
Email: [email protected]

  •  Accepted: 03 November 2011
  •  Published: 30 November 2011


Algebraic automata is getting much importance in theoretical computer science because of its various applications, for example, in optimization of programs, verification of protocols, cryptography and modeling biological phenomena. Design of a complex system not only requires functionality but it also needs to capture its control behaviour. This paper is a part of our ongoing research on integration of algebraic automata and formal methods. Algebraic automaton is a powerful tool in modeling behaviour while Z is an ideal specification language used for describing statics of a system. Consequently, an integration of algebraic automata and Z will be a useful tool for modeling of complex systems. In this paper, we have described formal partitioning analysis of extended algebraic automata because of its use in components based modeling. At first, formal specification of constructing sub-automata for given automata is presented. Then equality of two given automata is verified. In next, cycles are identified and finally formal partitioning analysis of extended algebraic automata is provided. The formal specification is checked, analyzed and validated using Z/Eves tool.

Key words: Algebraic automata, partitioning automata, component based modeling, Z notation, validation.