Refinement in Formal Proof of Equivalence in Morphisms over Strongly Connected Algebraic Automata (Technical Report‪)‬

1. Introduction Almost all large, complex and critical systems are being controlled by computer software. When software is used in a complex system, for example, in a safety critical system its failure may cause a huge loss in terms of deaths, injuries or financial damages. Therefore, constructing correct software is as important as its other counterparts, for example, hardware or electromechanical systems [1]. Formal methods are approaches used for specification of properties of software and hardware systems insuring correctness of a system [2]. Using formal methods, we can describe a mathematical model and then it can be analyzed and validated increasing confidence over a system [3]. At the current stage of development in formal approaches, it is not possible to develop a system using a single formal technique and as a result its integration is required with other traditional approaches. That is why integration of approaches has become a well-researched area in computing systems [4,5,6,7,8,9,10]. Further, design of a complex system not only requires capturing functionality but it also needs to model its control behavior. There are a large variety of specification techniques which are suitable for specific aspects in the software development process. For example, algebraic techniques, Z, VDM, and B are usually used for defining data types while process algebra, petri nets and automata are some of the examples which are best suited for capturing dynamic aspects of systems [11]. Because of well-defined mathematical syntax and semantics of the formal techniques, it is required to identify, explore and develop relationships between such approaches for modeling of complete, consistent and correct computerized systems.