Modularization of typed Gurevich machines

An important problem of the representation of a big dynamic system as a number of interrelating typed Gurevich Machines (Abstract State Machines or just ASMs in the sequel) and the subsequent combination of the specifications of individual ASMs into the specification of the whole system is investigated in the paper. The structure of such a system is formally defined and a notion of external signature of a typed ASM is introduced. Two main operations for combining existing specifications (and their implementing ASMs) are suggested: import of existing typed ASMs by a new one and union of several typed ASMs into a new one. The syntax and semantics of the operations are formally defined.