17-03-2014, 08:52 PM
Abstract
Algebraic automaton has emerged with several
modern applications in computer science and
engineering. Design of theorem provers, development
of model checkers, optimization of programs are some
of its applications. The Z notation is suitable for
modeling static while automata are powerful for
describing dynamic parts of a system. Consequently,
their integration is required. In this paper, we have
proposed a relationship between the fundamentals of
algebraic automata and Z. Initially, we have given
formalization of the extended algebraic automata.
Then formal construction of homomorphism is
described and extended to isomorphism. Finally, a
formal procedure of conversion from homomorphism
(isomorphism) to endomorphism (automorphism) is
given. The formal specification is analyzed and
validated using Z/EVES tool.
1. Introduction
The use of computers to describe complex objects
and their interaction simulating reality in a manageable
and controllable manner proves its essence in the
advancement of information technology. Of course,
computers are being controlled by software systems
whose failure may cause a big loss. Consequently,
constructing correct software is as important as its
other counterparts, for example, hardware or electromechanical
systems [1]. Software specification is an
important tool introduced by software engineering for
improving quality. If the specification is given using
diagrams, notations or natural languages, then many
drawbacks are usually identified at later stages of the
software development. Formal methods are tools and
techniques for describing properties of software and
hardware systems. Because of rigorous computer tool
support, formal methods can be applied correctly to
remove ambiguities from software specification at
early stages of the software process. Using formal
methods, we can describe formal specifications and
then develop a mathematical model which can be
analyzed and validated increasing confidence over a
system under construction [2].
The software technology is growing and changing
so rapidly that at the current stage of development in
formal methods, it is not possible to develop a system
using a single formal technique. As a result, various
techniques have to be integrated at different levels of
development [3]. That is why integration of approaches
has become a well-researched area. Further, design of a
complex system not only requires functionality but it
also needs to model the control behavior. For example,
Z notation, VDM, and RAISE are usually used for
describing static part while petri-nets, automata and
process algebra are well suited for modeling dynamics
of a system [4]. Consequently, it is required to identify
the relationships between such techniques to model a
system completely considering both of its aspects.
Algebraic automaton has emerged with several
modern applications in computer science and
engineering. Design of theorem provers, development
of model checkers, optimization of programs are some
of its applications. The Z notation is suitable for
modeling static while automata are powerful for
describing dynamic parts of a system. Consequently,
their integration is required. In this paper, we have
proposed a relationship between the fundamentals of
algebraic automata and Z. Initially, we have given
formalization of the extended algebraic automata.
Then formal construction of homomorphism is
described and extended to isomorphism. Finally, a
formal procedure of conversion from homomorphism
(isomorphism) to endomorphism (automorphism) is
given. The formal specification is analyzed and
validated using Z/EVES tool.
1. Introduction
The use of computers to describe complex objects
and their interaction simulating reality in a manageable
and controllable manner proves its essence in the
advancement of information technology. Of course,
computers are being controlled by software systems
whose failure may cause a big loss. Consequently,
constructing correct software is as important as its
other counterparts, for example, hardware or electromechanical
systems [1]. Software specification is an
important tool introduced by software engineering for
improving quality. If the specification is given using
diagrams, notations or natural languages, then many
drawbacks are usually identified at later stages of the
software development. Formal methods are tools and
techniques for describing properties of software and
hardware systems. Because of rigorous computer tool
support, formal methods can be applied correctly to
remove ambiguities from software specification at
early stages of the software process. Using formal
methods, we can describe formal specifications and
then develop a mathematical model which can be
analyzed and validated increasing confidence over a
system under construction [2].
The software technology is growing and changing
so rapidly that at the current stage of development in
formal methods, it is not possible to develop a system
using a single formal technique. As a result, various
techniques have to be integrated at different levels of
development [3]. That is why integration of approaches
has become a well-researched area. Further, design of a
complex system not only requires functionality but it
also needs to model the control behavior. For example,
Z notation, VDM, and RAISE are usually used for
describing static part while petri-nets, automata and
process algebra are well suited for modeling dynamics
of a system [4]. Consequently, it is required to identify
the relationships between such techniques to model a
system completely considering both of its aspects.