Refinement in Formal Proof of Equivalence in Morphisms over Strongly Connected Algebraic Automata

Nazir Ahmad Zafar, Ajmal Hussain, Amir Ali

.

DOI: 10.4236/jsea.2009.22012                

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.

Keywords

Formal Methods, Automata, Integration of Approaches, Z Notation, Validation

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	[1] Hall, “Correctness by construction: Integrating formality into a commercial development process,” LNCS, Springer, Vol. 2391, pp. 139-157, 2002.
[2]	[2] J. Burgess, “The role of formal methods in software en-gineering education and industry,” Technical Report: CS-EXT-1995-045, University of Bristol, UK, 1995.
[3]	[3] A. L. Gwandu and D. J. Creasey, “The importance of formal specification in the design of hardware systems,” School of Electron & Electrical Engineering, Birming-ham University, UK, 1994.
[4]	[4] H. A. Gabbar, “Fundamentals of formal methods,” Mod-ern Formal Methods and Applications, Springer, 2006.
[5]	[5] A. Boiten, et al., “Integrated formal methods (IFM04),” Springer, 2004.
[6]	[6] J. Davies and J. Gibbons, “Integrated formal methods (IFM07),” UK, Springer, 2007.
[7]	[7] J. Romijn, G. Smith, and J. V. D. Pol, “Integrated formal methods (IFM 05),” Springer, 2005.
[8]	[8] K. Araki, A. Galloway, and K. Taguchi, “Integrated for-mal methods (IFM99),” Springer, 1999.
[9]	[9] R. Bussow and W. Grieskamp, “A modular framework for the integration of heterogeneous notations and tools,” Proceedings of the 1st International Conference on Inte-grated Formal Methods, UK, Springer, pp. 211-230, 1999.
[10]	[10] W. Grieskamp, T. Santen, and B. Stoddart, “Integrated formal methods (IFM 2000),” Germany, Springer, 2000.
[11]	[11] T. B. Raymond, “Integrating formal methods by unifying abstractions,” LNCS, Springer, Vol. 2999, pp. 441-460, 2004.
[12]	[12] J. S. Dong, R. Duke, and P. Hao, “Integrating object-Z with timed automata,” in Proceedings of the 10th IEEE International Conference on Engineering of Complex Computer Systems, pp. 488-497, 2005.
[13]	[13] S. Dong, et al., “Timed patterns: TCOZ to timed auto-mata,” in the 6th IEEE International Conference on For-mal Engineering Methods, USA, 2004.
[14]	[14] R. L. Constable, et al., “Formalizing automata II: Decid-able properties,” Cornell University, 1997.
[15]	[15] R. L. Constable, et al., “Constructively formalizing automata theory,” Foundations of Computing Series, MIT Press, 2000.
[16]	[16] X. He, “Pz nets a formal method integrating Petri nets with Z,” Information & Software Technology, Vol. 43, No.1, pp. 1–18, 2001.
[17]	[17] M. Heiner and M. Heisel, “Modeling safety critical sys-tems with Z and Petri nets,” International Conference on Computer Safety, Reliability and Security, LNCS, Springer, Vol. 1698, pp. 361–374, 1999.
[18]	[18] H. Leading and J. Souquieres, “Integration of UML and B specification techniques: Systematic transformation from OCL expressions into B,” in the Proceedings of Asia-Pacific Software Engineering Conference (APSEC 02), Australia, 2002.
[19]	[19] H. Leading and J. Souquieres, “Integration of UML views using B notation,” in the Proceedings of Workshop on Integration and Transformation of UML Models, Spain, 2002.
[20]	[20] W. Wechler, “The concept of fuzziness in automata and language theory,” Akademic-Verlag, Berlin, 1978.
[21]	[21] N. M. John and S. M. Davender, “Fuzzy automata and languages: Theory and applications,” Chapman & HALL, 2002.
[22]	[22] M. Ito, “Algebraic theory of automata and languages,” World Scientific Publishing, 2004.
[23]	[23] K. Kaynar and N. Lynchn, “The theory of timed I/O automata,” Morgan & Claypool Publishers, 2006.
[24]	[24] C. Godsil and G. Royle, “Algebraic graph theory,” Springer, 2001.
[25]	[25] Z. Aleksic, “From biology to computation,” IOS Press Publishers, 1993.
[26]	[26] L. B. Kier, P. G. Seybold, and C. K. Cheng, “Modeling chemical systems using cellular automata,” Springer, 2005.
[27]	[27] T. Ellman, “Specification and synthesis of hybrid auto-mata for physics-based animation,” Automated Software Engineering, Vol. 13, No. 3, pp. 395–418, 2006.
[28]	[28] D. Conrad and B. Hotzer, “Selective integration of formal methods in development of electronic control units,” in Proceedings of 2nd International Conference on Formal Engineering Methods, Vol. 9, No. 11, pp.144–155, 1998.
[29]	[29] M. Brendan and J. S. Dong, “Blending object-Z and timed CSP: An introduction to TCOZ,” in Proceedings of the 1998 International Conference on Software Engi-neering, Vol. 19, No. 25, pp. 95–104, 1998.
[30]	[30] J. V. Guttag and J. J. Horning, “The algebraic specifica-tion of abstract data types,” Acta Informatica, Springer Berlin, pp. 27–52, 2004.
[31]	[31] A. T. Nakagawa, et al., “Cafe an industrial-strength alge-braic formal method,” Elsevier Science & Technology, 2000.
[32]	[32] J. M. Spivey, “The Z notation: A reference manual,” Prentice Hall, 1989.
[33]	[33] J. M. Wing, “A specifier: Introduction to formal meth-ods,” IEEE Computer, Vol. 23, No. 9, pp. 8–24, 1990.
[34]	[34] J. Woodcock and J. Davies, “Using Z: Specification, refinement and proof,” Prentice Hall International, 1996.
[35]	[35] J. A. Anderson, “Automata theory with modern applica-tions,” Cambridge University Press, 2006.
[36]	[36] L. L. Claudio, et al., “Applications of finite automata representing large vocabularies,” Software Practice & Experience, Vol. 23, No. 1, pp. 15–30, 1993.
[37]	[37] Y. V. Moshe, “Nontraditional applications of automata theory,” Theoretical Aspects of Computer Software, 1994.
[38]	[38] D. I. A. Cohen, “Introduction to computer theory,” 2nd Edition, John Wiley & Sons Inc., 1996.
[39]	[39] N. A. Zafar, A. Hussain, and A. Ali, “Formal proof of equivalence in endomorphisms and automorphisms over strongly connected automata,” International Conference on Computer Science and Software Engineering (CSSE 2008), Wuhan, China, 2008.
[40]	[40] D. P. Tuan, “Computing with words in formal methods,” University of Canberra, Australia, 2000.
[41]	[41] J. P. Bowen, “Formal specification and documentation using Z: A case study approach,” International Thomson Computer Press, 1996.
[42]	[42] S. A. Vilkomir and J. P. Bowen, “Formalization of soft-ware testing criterion,” South Bank University, London, 2001.
[43]	[43] C. T. Chou, “A formal theory of undirected graphs in higher order logic,” in Proceedings of 7th International Workshop on Higher Order Logic, Theorem Proving and Application, LNCS, Vol. 859, pp. 144–157, 1994.