Construction of Intersection of Nondeterministic Finite Automata using Z Notation

Authors: Nazir Ahmad Zafar, Nabeel Sabir, Amir Ali

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.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1079936

References:

[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.