Verifying Monoid and Group Morphisms over Strongly Connected Algebraic Automata

Nazir Ahmad Zafar, Ajmal Hussain, Amir Ali

.

DOI: 10.4236/jsea.2010.38093                

Abstract

Automata theory has played an important role in theoretical computer science since last couple of decades. The alge-braic automaton has emerged with several modern applications, for example, optimization of programs, design of model checkers, development of theorem provers because of having certain interesting properties and structures from algebraic theory of mathematics. Design of a complex system requires functionality and also needs to model its control behavior. Z notation has proved to be an effective tool for describing state space of a system and then defining operations over it. Consequently, an integration of algebraic automata and Z will be a useful computer tool which can be used for modeling of complex systems. In this paper, we have linked algebraic automata and Z defining a relationship between fundamentals of these approaches which is refinement of our previous work. At first, we have described strongly connected algebraic automata. Then homomorphism and its variants over strongly connected automata are specified. Next, monoid endomorphisms and group automorphisms are formalized. Finally, equivalence of endomorphisms and automorphisms under certain assumptions are described. The specification is analyzed and validated using Z/Eves toolset.

Keywords

Formal Methods, Z notation, Algebraic Automata, Validation and Verification

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	A. Hall, “Correctness by Construction: Integrating Formality into a Commercial Development Process,” Lecture Notes in Computer Science, Springer, Vol. 2391, 2002, pp. 139-157.
[2]	C. J. Burgess, “The Role of Formal Methods in Software Engineering Education and Industry,” Technical Report: CS-EXT-1995-045, University of Bristol, Bristol, 1995.
[3]	B. A. L. Gwandu and D. J. Creasey, “The Importance of Formal Specification in the Design of Hardware Systems,” School of Electron & Electrical Engineering, Birmingham University, Birmingham, 1994.
[4]	H. A. Gabbar, “Fundamentals of Formal Methods,” Modern Formal Methods and Applications, Springer Netherlands, 2006.
[5]	E. A. Boiten, et al., “Integrated Formal Methods (IFM 04),” Springer, Canterbury, 2004.
[6]	J. Davies and J. Gibbons, “Integrated Formal Methods (IFM07),” UK, Springer, 2007.
[7]	J. Romijn, G. Smith and J. V. D. Pol, “Integrated Formal Methods (IFM 05),” Springer, Eindhoven, 2005.
[8]	K. Araki, A. Galloway and K. Taguchi, “Integrated Formal Methods (IFM99),” Springer, York, 1999.
[9]	R. Bussow and W. Grieskamp, “A Modular Framework for Integration of Heterogeneous Notations and Tools,” Integrated Formal Methods (IFM 99), Springer-Verlag, York, 1999, pp. 211-230.
[10]	W. Grieskamp, T. Santen and B. Stoddart, “Integrated Formal Methods,” Springer, Dagstuhl Castle, 2000.
[11]	T. B. Raymond, “Integrating Formal Methods by Unifying Abstractions,” Lecture Notes in Computer Science, Springer, Vol. 2999, 2004, pp. 441-460.
[12]	J. S. Dong, R. Duke and P. Hao, “Integrating Object-Z with Timed Automata,” 12th IEEE International Conference on Engineering Complex Computer Systems, Auckland, 2005, pp. 488-497.
[13]	S. Dong, et al., “Timed Patterns: TCOZ to Timed Automata,” 6th International Conference on Formal Engineering Methods, Seattle, 2004, pp. 483-498.
[14]	R. L. Constable, et al., “Formalizing Automata II: Decidable Properties,” Cornell University, New York, 1997.
[15]	R. L. Constable, et al., “Constructively Formalizing Automata Theory,” Foundations of Computing Series, MIT Press, Cambridge, 2000.
[16]	X. He, “Pz Nets a Formal Method Integrating Petri Nets with Z,” Information & Software Technology, Vol. 43, No. 1, 2001, pp. 1-18.
[17]	M. Heiner and M. Heisel, “Modeling Safety Critical Systems with Z and Petri Nets,” International Conference on Computer Safety, Reliability and Security, Springer, Lecture Notes In Computer Science, Toulouse, Vol. 1698, 1999, pp. 361-374.
[18]	H. Leading and J. Souquieres, “Integration of UML and B Specification Techniques: Systematic Transformation from OCL Expressions into B,” Asia-Pacific Software Engineering Conference, Gold Coast, 2002, pp. 495-504.
[19]	H. Leading and J. Souquieres, “Integration of UML Views using B Notation,” Proceeding of Workshop on Integration and Transformation of UML Models, Málaga, 2002.
[20]	W. Wechler, “The Concept of Fuzziness in Automata and Language Theory,” Akademic-Verlag, Berlin, 1978.
[21]	N. M. John and S. M. Davender, “Fuzzy Automata and Languages: Theory and Applications,” Chapman & Hall, CRC, USA, 2002.
[22]	M. Ito, “Algebraic Theory of Automata and Languages,” World Scientific Publishing, Singapore, 2004.
[23]	D. K. Kaynar and N. Lynchn, “The Theory of Timed I/O Automata,” Morgan & Claypool, 2006.
[24]	C. Godsil and G. Royle, “Algebraic Graph Theory,” Springer, New York, 2001.
[25]	Z. Aleksic, “From Biology to Computation,” IOS Press Publishers, IOS Press, Amsterdam, 1993.
[26]	L. B. Kier, P. G. Seybold and C. K. Cheng, “Modeling Chemical Systems Using Cellular Automata,” Springer, New York, 2005.
[27]	T. Ellman, “Specification and Synthesis of Hybrid Automata for Physics-based Animation,” Automated Software Engineering, Vol. 13, No. 3, 2006, pp. 395-418.
[28]	N. A. Zafar, A. Hussain and A. Ali, “Refinement: Formal Proof of Equivalence in Endomorphisms and Automorphisms over Strongly Connected Automata,” Journal of Software Engineering and Applications, Vol. 2, No. 2, 2009, pp. 77-85.
[29]	N. A. Zafar, A. Hussain and A. Ali, “Formal Proof of Equivalence in Endomorphisms and Automorphisms over Strongly Connected Automata,” Proceedings of the 2008 International Conference on Computer Science and Software Engineering, Wuhan, Vol. 2, 2008, pp. 792-795.
[30]	D. P. Tuan, “Computing with Words in Formal Methods,” University of Canberra, Canberra, Australia, 2000.
[31]	M. Conrad and D. H?tzer, “Selective Integration of Formal Methods in Development of Electronic Control Units,” Proceedings of the 2nd IEEE International Conference on Formal Engineering Methods, Brisbane, 1998, pp.144-155.
[32]	M. Brendan and J. S. Dong, “Blending Object-Z and Timed CSP: An Introduction to TCOZ,” Proceedings of the 20th International Conference on Software Engineering, Kyoto, 1998, pp. 95-104.
[33]	A. T. Nakagawa, et al., “Cafe an Industrial-Strength Algebraic Formal Method,” Elsevier Science & Technology, Amsterdam, 2000.
[34]	J. V. Guttag and J. J. Horning, “The Algebraic Specification of Abstract Data Types,” Acta Informatica, Springer Berlin, Vol. 10, No. 1, 2004, pp. 27-52.
[35]	J. M. Spivey, “The Z Notation: A Reference Manual,” International Series in Computer Science, Prentice Hall, 1989.
[36]	J. M. Wing, “A Specifier: Introduction to Formal Methods,” IEEE Computer, Vol. 23, No. 9, 1990, pp. 8-24.
[37]	J. Woodcock and J. Davies, “Using Z: Specification, Refinement and Proof,” Prentice Hall, International Series in Computer Science, 1996.
[38]	J. A. Anderson, “Automata Theory with Modern Applications,” Cambridge University Press, Cambridge, 2006.
[39]	L. L. Claudio, et al., “Applications of Finite Automata Representing Large Vocabularies,” Software Practice & Experience, Vol. 23, No. 1, 1993, pp. 15-30.
[40]	Y. V. Moshe, “Nontraditional Applications of Automata Theory,” Proceedings of the International Conference on Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, Vol. 789, Sendai, 1994, pp. 575-597.
[41]	D. I. A. Cohen, “Introduction to Computer Theory,” 2nd Edition, John Wiley & Sons Inc., New York, 1996.
[42]	J. P. Bowen, “Formal Specification and Documentation Using Z: A Case Study Approach,” International Thomson Computer Press, London, 1996.
[43]	S. A. Vilkomir and J. P. Bowen, “Formalization of Software Testing Criterion,” South Bank University, London, 2001.
[44]	C. T. Chou, “A Formal Theory of Undirected Graphs in Higher Order Logic,” Proceeding of 7th International Workshop on Higher Order Logic, Lecture Notes in Computer Science, Valletta, Vol. 859, 1994, pp. 144-157.