Linking Finite Automata and Formal Methods Enhancing Modeling Power for Complex Systems
Nabeel Sabir, Amir Ali, Nazir Ahmad Zafar · 2008
Automata have various applications and it plays an important role in computer science, particularly, in modeling behavior of systems. Z notation is an ideal one to be used defining state space of a system and then operations over it. Consequently, it requires an integration of automata and Z increasing its modeling power. Further, finite automata may have different implementations therefore if we give a mathematical analysis and describe formal specification of it before implementing then correctness of a model can be argued. Formal methods are rigorous mathematical techniques which can be used for specification of software systems. To achieve an objective of integration of approaches, we have combined automata and Z. Formalism of this relationship is analyzed and validated using Z/EVES tool.