Construction of Intersection of Nondeterministic Finite Automata using Z Notation
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.
[1] M. Y. Vardi, and T. Wilke, "Automata - from logic to
algorithms," Logic and Automata - History and Perspectives, 2007.
[2] J. M. Spivey, "The Z notation, A Reference Manual," Englewood Cliffs,
NJ, Prentice-Hall, 1989.
[3] I. J. Holub, "Finding Common Motifs with Gaps using Finite
Automata," In Implementation and Application of Automata, Springer-
Verlag, pp: 69-77, ISBN 3-540-37213-X, 2006.
[4] K. Brouwer, W. Gellerich and E. Ploedereder, "Myths and Facts about
the Efficient Implementation of Finite Automata and Lexical Analysis,"
Springer-Berlin, ISBN 978-3-540-64304-3, 2006.
[5] I. Meisels and M. Saaltink, "The Z/EVES Reference Manual," TR-97-
5493-03, ORA Canada, CANADA, 1997.
[6] E. A. Boiten, J. Derrick and G. Smith, "Integrated Formal Methods
(IFM 2004)," Canterbury, UK, Springer-Verlag, 2004.
[7] J. Davies and J. Gibbons, "Integrated Formal Methods (IFM 2007),"
Oxford, UK, Springer-Verlag, 2007.
[8] J. Romijn, G. Smith and J. v. d. Pol, "Integrated Formal Methods (IFM
2005)," Eindhoven, The Netherlands, Springer-Verlag, 2005.
[9] K. Araki, A. Galloway and K. Taguchi, "Integrated Formal Methods
(IFM 99)," York, UK, Springer-Verlag, 1999.
[10] M. Butler, L. Petre and K. Sere, "Integrated Formal Methods (IFM
2002)," Turku, Finland, Springer-Verlag, 2002.
[11] W. Grieskamp, T. Santen and B. Stoddart, "Integrated Formal Methods
(IFM 2000)," Dagstuhl Castle, Germany, Springer-Verlag, 2000.
[12] J. S. Dong, R. Duke and P. Hao, "Integrating Object-Z with Timed
Automata," 12th IEEE International Conference on Engineering
Complex Computer Systems (ICECCS 2005), pp: 488-497, 2005.
[13] J. S. Dong et al, "Timed Patterns: TCOZ to Timed Automata," 6th
International Conference on Formal Engineering Methods (ICFEM-04),
LNCS, pp: 483-498, 2004.
[14] R. L. Constable, P. B. Jackson, P. Naumov and J. Uribe, "Formalizing
Automata II: Decidable Properties," Cornell University, 1997.
[15] R. L. Constable, P. B. Jackson, P. Naumov and J. Uribe,
"Constructively Formalizing Automata Theory," Foundations Of
Computing Series, MIT Press, ISBN:0-262-16188-5, 2000.
[16] R. Bussow and W. Grieskamp, "A Modular Framework for the
Integration of Heterogeneous Notations and Tools," Integrated Formal
Methods (IFM 99), York, UK, Springer-Verlag, pp: 211-230, 1999.
[17] R. B├╝ssow, R. Geisler and M. Klar, "Specifying Safety-Critical
Embedded Systems with Statecharts and Z: A Case Study,"
Fundamental Approaches to Software Engineering, Springer Berlin,
ISBN, 978-3-540-64303-6, 2004.
[18] M. Heiner and M. Heisel, "Modeling safety-critical systems with Z and
Petri nets," International Conference on Computer Safety, Reliability
and Security, LNCS, Springer, pp: 361-374, 1999.
[19] X. He, "Pz nets a formal method integrating petri nets with z,"
Information & Software Technology, 43(1), pp: 1-18, 2001.
[20] H. Leading and J. Souquieres, "Integration of UML and B Specification
Techniques: Systematic Transformation from OCL Expressions into B,"
Proceedings of Asia-Pacific Software Engineering Conference
(APSEC02), Australia, 2002.
[21] H. Leading and J. Souquieres, "Integration of UML Views using B
Notation," Proceedings of Workshop on Integration and Transformation
of UML models (WITUML02), Spain, 2002.
[22] C. Heitmeyer, "On the Need for Practical Formal Methods," Lecture
Notes in Computer Science, Vol.1486, pp: 18-26, 1998.
[23] E. Ciapessoni, A. C. Porisini, E. Crivelli, D. Mandrioli, P. Mirandola
and A. Morzenti, "From Formal Models to Formally-Based Methods:
An Industrial Experience," TOSEM, Vol.8, No.1, pp: 79-113, 1999.
[24] J. P. Bowen, "Ten Commandments of Formal Methods," IEEE
Computer, Vol.28, No.4, pp: 56-63, 1995.
[25] J. P. Bowen and M. G. Hinchey, "The Use of Industrial-Strength of
Formal Methods," Proceedings of 21st International Computer Software
& Application Conference (COMPSAC'97), pp: 332-337, 1997.
[26] M. Barjaktarovic, "The State-of-the-Art in Formal Methods," AFOSR
Summer Research Technical Report for Rome Research Site, Formal
Methods Framework-Monthly Status Report, F30602-99-C-0166,
WetStone Technologies, 1998.
[27] R. W. Butler, "What is Formal Methods?," NASA LaRC Formal
Methods Program, 2001.
[28] S. Easterbrook, R. Lutz, R. Covington, J. Kelly, Y. Ampo and D.
Hamilton, "Experiences Using Lightweight Formal Methods for
Requirements Modeling," IEEE Transactions on Software Engineering,
Vol.24, No.1, pp: 4-14, 1998.
[29] J. M. Wing, "A Specifier-s Introduction to Formal Methods," IEEE
Computer, Vol.23, No.9, pp: 8-24, 1990.
[30] H. A. Gabbar, "Fundamentals of Formal Methods, Modern Formal
Methods and Applications," Springer Netherlands, ISBN, 978-1-4020-
4222-5, 2006.
[31] J. E. Hopcroft, R. Motwani and J. D. Ullman, "Introduction to Automata
Theory, Language and Computation," Addison-Wesley, Reading, 2001.
[32] M. Sipser, "Introduction to the Theory of Computation," Course
Technology, ISBN-13: 9780534950972, 2005.
[33] C. T. Chou, "A Formal Theory of Undirected Graphs in Higher Order
Logic," 7th International Workshop on Higher Order Logic Theorem
Proving and Application, pp: 144-157, 1994.
[1] M. Y. Vardi, and T. Wilke, "Automata - from logic to
algorithms," Logic and Automata - History and Perspectives, 2007.
[2] J. M. Spivey, "The Z notation, A Reference Manual," Englewood Cliffs,
NJ, Prentice-Hall, 1989.
[3] I. J. Holub, "Finding Common Motifs with Gaps using Finite
Automata," In Implementation and Application of Automata, Springer-
Verlag, pp: 69-77, ISBN 3-540-37213-X, 2006.
[4] K. Brouwer, W. Gellerich and E. Ploedereder, "Myths and Facts about
the Efficient Implementation of Finite Automata and Lexical Analysis,"
Springer-Berlin, ISBN 978-3-540-64304-3, 2006.
[5] I. Meisels and M. Saaltink, "The Z/EVES Reference Manual," TR-97-
5493-03, ORA Canada, CANADA, 1997.
[6] E. A. Boiten, J. Derrick and G. Smith, "Integrated Formal Methods
(IFM 2004)," Canterbury, UK, Springer-Verlag, 2004.
[7] J. Davies and J. Gibbons, "Integrated Formal Methods (IFM 2007),"
Oxford, UK, Springer-Verlag, 2007.
[8] J. Romijn, G. Smith and J. v. d. Pol, "Integrated Formal Methods (IFM
2005)," Eindhoven, The Netherlands, Springer-Verlag, 2005.
[9] K. Araki, A. Galloway and K. Taguchi, "Integrated Formal Methods
(IFM 99)," York, UK, Springer-Verlag, 1999.
[10] M. Butler, L. Petre and K. Sere, "Integrated Formal Methods (IFM
2002)," Turku, Finland, Springer-Verlag, 2002.
[11] W. Grieskamp, T. Santen and B. Stoddart, "Integrated Formal Methods
(IFM 2000)," Dagstuhl Castle, Germany, Springer-Verlag, 2000.
[12] J. S. Dong, R. Duke and P. Hao, "Integrating Object-Z with Timed
Automata," 12th IEEE International Conference on Engineering
Complex Computer Systems (ICECCS 2005), pp: 488-497, 2005.
[13] J. S. Dong et al, "Timed Patterns: TCOZ to Timed Automata," 6th
International Conference on Formal Engineering Methods (ICFEM-04),
LNCS, pp: 483-498, 2004.
[14] R. L. Constable, P. B. Jackson, P. Naumov and J. Uribe, "Formalizing
Automata II: Decidable Properties," Cornell University, 1997.
[15] R. L. Constable, P. B. Jackson, P. Naumov and J. Uribe,
"Constructively Formalizing Automata Theory," Foundations Of
Computing Series, MIT Press, ISBN:0-262-16188-5, 2000.
[16] R. Bussow and W. Grieskamp, "A Modular Framework for the
Integration of Heterogeneous Notations and Tools," Integrated Formal
Methods (IFM 99), York, UK, Springer-Verlag, pp: 211-230, 1999.
[17] R. B├╝ssow, R. Geisler and M. Klar, "Specifying Safety-Critical
Embedded Systems with Statecharts and Z: A Case Study,"
Fundamental Approaches to Software Engineering, Springer Berlin,
ISBN, 978-3-540-64303-6, 2004.
[18] M. Heiner and M. Heisel, "Modeling safety-critical systems with Z and
Petri nets," International Conference on Computer Safety, Reliability
and Security, LNCS, Springer, pp: 361-374, 1999.
[19] X. He, "Pz nets a formal method integrating petri nets with z,"
Information & Software Technology, 43(1), pp: 1-18, 2001.
[20] H. Leading and J. Souquieres, "Integration of UML and B Specification
Techniques: Systematic Transformation from OCL Expressions into B,"
Proceedings of Asia-Pacific Software Engineering Conference
(APSEC02), Australia, 2002.
[21] H. Leading and J. Souquieres, "Integration of UML Views using B
Notation," Proceedings of Workshop on Integration and Transformation
of UML models (WITUML02), Spain, 2002.
[22] C. Heitmeyer, "On the Need for Practical Formal Methods," Lecture
Notes in Computer Science, Vol.1486, pp: 18-26, 1998.
[23] E. Ciapessoni, A. C. Porisini, E. Crivelli, D. Mandrioli, P. Mirandola
and A. Morzenti, "From Formal Models to Formally-Based Methods:
An Industrial Experience," TOSEM, Vol.8, No.1, pp: 79-113, 1999.
[24] J. P. Bowen, "Ten Commandments of Formal Methods," IEEE
Computer, Vol.28, No.4, pp: 56-63, 1995.
[25] J. P. Bowen and M. G. Hinchey, "The Use of Industrial-Strength of
Formal Methods," Proceedings of 21st International Computer Software
& Application Conference (COMPSAC'97), pp: 332-337, 1997.
[26] M. Barjaktarovic, "The State-of-the-Art in Formal Methods," AFOSR
Summer Research Technical Report for Rome Research Site, Formal
Methods Framework-Monthly Status Report, F30602-99-C-0166,
WetStone Technologies, 1998.
[27] R. W. Butler, "What is Formal Methods?," NASA LaRC Formal
Methods Program, 2001.
[28] S. Easterbrook, R. Lutz, R. Covington, J. Kelly, Y. Ampo and D.
Hamilton, "Experiences Using Lightweight Formal Methods for
Requirements Modeling," IEEE Transactions on Software Engineering,
Vol.24, No.1, pp: 4-14, 1998.
[29] J. M. Wing, "A Specifier-s Introduction to Formal Methods," IEEE
Computer, Vol.23, No.9, pp: 8-24, 1990.
[30] H. A. Gabbar, "Fundamentals of Formal Methods, Modern Formal
Methods and Applications," Springer Netherlands, ISBN, 978-1-4020-
4222-5, 2006.
[31] J. E. Hopcroft, R. Motwani and J. D. Ullman, "Introduction to Automata
Theory, Language and Computation," Addison-Wesley, Reading, 2001.
[32] M. Sipser, "Introduction to the Theory of Computation," Course
Technology, ISBN-13: 9780534950972, 2005.
[33] C. T. Chou, "A Formal Theory of Undirected Graphs in Higher Order
Logic," 7th International Workshop on Higher Order Logic Theorem
Proving and Application, pp: 144-157, 1994.
@article{"International Journal of Information, Control and Computer Sciences:61825", author = "Nazir Ahmad Zafar and Nabeel Sabir and Amir Ali", title = "Construction of Intersection of Nondeterministic Finite Automata using Z Notation", abstract = "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.", keywords = "Modeling, Nondeterministic finite automata, Znotation, Integration of approaches, Validation.", volume = "2", number = "4", pages = "1261-6", }
