{"references": ["M. Y. Vardi, and T. Wilke, \"Automata - from logic to\nalgorithms,\" Logic and Automata - History and Perspectives, 2007.", "J. M. Spivey, \"The Z notation, A Reference Manual,\" Englewood Cliffs,\nNJ, Prentice-Hall, 1989.", "I. J. Holub, \"Finding Common Motifs with Gaps using Finite\nAutomata,\" In Implementation and Application of Automata, Springer-\nVerlag, pp: 69-77, ISBN 3-540-37213-X, 2006.", "K. Brouwer, W. Gellerich and E. Ploedereder, \"Myths and Facts about\nthe Efficient Implementation of Finite Automata and Lexical Analysis,\"\nSpringer-Berlin, ISBN 978-3-540-64304-3, 2006.", "I. Meisels and M. Saaltink, \"The Z/EVES Reference Manual,\" TR-97-\n5493-03, ORA Canada, CANADA, 1997.", "E. A. Boiten, J. Derrick and G. Smith, \"Integrated Formal Methods\n(IFM 2004),\" Canterbury, UK, Springer-Verlag, 2004.", "J. Davies and J. Gibbons, \"Integrated Formal Methods (IFM 2007),\"\nOxford, UK, Springer-Verlag, 2007.", "J. Romijn, G. Smith and J. v. d. Pol, \"Integrated Formal Methods (IFM\n2005),\" Eindhoven, The Netherlands, Springer-Verlag, 2005.", "K. Araki, A. Galloway and K. Taguchi, \"Integrated Formal Methods\n(IFM 99),\" York, UK, Springer-Verlag, 1999.\n[10] M. Butler, L. Petre and K. Sere, \"Integrated Formal Methods (IFM\n2002),\" Turku, Finland, Springer-Verlag, 2002.\n[11] W. Grieskamp, T. Santen and B. Stoddart, \"Integrated Formal Methods\n(IFM 2000),\" Dagstuhl Castle, Germany, Springer-Verlag, 2000.\n[12] J. S. Dong, R. Duke and P. Hao, \"Integrating Object-Z with Timed\nAutomata,\" 12th IEEE International Conference on Engineering\nComplex Computer Systems (ICECCS 2005), pp: 488-497, 2005.\n[13] J. S. Dong et al, \"Timed Patterns: TCOZ to Timed Automata,\" 6th\nInternational Conference on Formal Engineering Methods (ICFEM-04),\nLNCS, pp: 483-498, 2004.\n[14] R. L. Constable, P. B. Jackson, P. Naumov and J. Uribe, \"Formalizing\nAutomata II: Decidable Properties,\" Cornell University, 1997.\n[15] R. L. Constable, P. B. Jackson, P. Naumov and J. Uribe,\n\"Constructively Formalizing Automata Theory,\" Foundations Of\nComputing Series, MIT Press, ISBN:0-262-16188-5, 2000.\n[16] R. Bussow and W. Grieskamp, \"A Modular Framework for the\nIntegration of Heterogeneous Notations and Tools,\" Integrated Formal\nMethods (IFM 99), York, UK, Springer-Verlag, pp: 211-230, 1999.\n[17] R. B\u251c\u255dssow, R. Geisler and M. Klar, \"Specifying Safety-Critical\nEmbedded Systems with Statecharts and Z: A Case Study,\"\nFundamental Approaches to Software Engineering, Springer Berlin,\nISBN, 978-3-540-64303-6, 2004.\n[18] M. Heiner and M. Heisel, \"Modeling safety-critical systems with Z and\nPetri nets,\" International Conference on Computer Safety, Reliability\nand Security, LNCS, Springer, pp: 361-374, 1999.\n[19] X. He, \"Pz nets a formal method integrating petri nets with z,\"\nInformation & Software Technology, 43(1), pp: 1-18, 2001.\n[20] H. Leading and J. Souquieres, \"Integration of UML and B Specification\nTechniques: Systematic Transformation from OCL Expressions into B,\"\nProceedings of Asia-Pacific Software Engineering Conference\n(APSEC02), Australia, 2002.\n[21] H. Leading and J. Souquieres, \"Integration of UML Views using B\nNotation,\" Proceedings of Workshop on Integration and Transformation\nof UML models (WITUML02), Spain, 2002.\n[22] C. Heitmeyer, \"On the Need for Practical Formal Methods,\" Lecture\nNotes in Computer Science, Vol.1486, pp: 18-26, 1998.\n[23] E. Ciapessoni, A. C. Porisini, E. Crivelli, D. Mandrioli, P. Mirandola\nand A. Morzenti, \"From Formal Models to Formally-Based Methods:\nAn Industrial Experience,\" TOSEM, Vol.8, No.1, pp: 79-113, 1999.\n[24] J. P. Bowen, \"Ten Commandments of Formal Methods,\" IEEE\nComputer, Vol.28, No.4, pp: 56-63, 1995.\n[25] J. P. Bowen and M. G. Hinchey, \"The Use of Industrial-Strength of\nFormal Methods,\" Proceedings of 21st International Computer Software\n& Application Conference (COMPSAC'97), pp: 332-337, 1997.\n[26] M. Barjaktarovic, \"The State-of-the-Art in Formal Methods,\" AFOSR\nSummer Research Technical Report for Rome Research Site, Formal\nMethods Framework-Monthly Status Report, F30602-99-C-0166,\nWetStone Technologies, 1998.\n[27] R. W. Butler, \"What is Formal Methods?,\" NASA LaRC Formal\nMethods Program, 2001.\n[28] S. Easterbrook, R. Lutz, R. Covington, J. Kelly, Y. Ampo and D.\nHamilton, \"Experiences Using Lightweight Formal Methods for\nRequirements Modeling,\" IEEE Transactions on Software Engineering,\nVol.24, No.1, pp: 4-14, 1998.\n[29] J. M. Wing, \"A Specifier-s Introduction to Formal Methods,\" IEEE\nComputer, Vol.23, No.9, pp: 8-24, 1990.\n[30] H. A. Gabbar, \"Fundamentals of Formal Methods, Modern Formal\nMethods and Applications,\" Springer Netherlands, ISBN, 978-1-4020-\n4222-5, 2006.\n[31] J. E. Hopcroft, R. Motwani and J. D. Ullman, \"Introduction to Automata\nTheory, Language and Computation,\" Addison-Wesley, Reading, 2001.\n[32] M. Sipser, \"Introduction to the Theory of Computation,\" Course\nTechnology, ISBN-13: 9780534950972, 2005.\n[33] C. T. Chou, \"A Formal Theory of Undirected Graphs in Higher Order\nLogic,\" 7th International Workshop on Higher Order Logic Theorem\nProving and Application, pp: 144-157, 1994."]}

Functionalities and control behavior are both primary requirements in design of a complex system. Automata theory plays an important role in modeling behavior of a system. Z is an ideal notation which is used for describing state space of a system and then defining operations over it. Consequently, an integration of automata and Z will be an effective tool for increasing modeling power for a complex system. Further, nondeterministic finite automata (NFA) may have different implementations and therefore it is needed to verify the transformation from diagrams to a code. If we describe formal specification of an NFA before implementing it, then confidence over transformation can be increased. In this paper, we have given a procedure for integrating NFA and Z. Complement of a special type of NFA is defined. Then union of two NFAs is formalized after defining their complements. Finally, formal construction of intersection of NFAs is described. The specification of this relationship is analyzed and validated using Z/EVES tool.