The GAT approach to specifying mixed systems

This paper outlines a practical use of algebraic specifications for the development of heterogeneous software systems. This kind of systems mixes several viewpoints, e.g. static, functional and dynamic aspects. Writing, from scratch, an algebraic specification for such systems is quite difficult, so we developed the concept of Graphic Abstract Data Type (GAT). In this paper we present a method to build an algebraic specification of a sequential system via a symbolic transition system (STS). The STS models both the dynamic aspects and the static aspects of the system. The STS is also the basis of an algorithm that computes the functional aspects of the system (an algebraic specification). Computing the specification is partly automatic, this improves the compatibility between the aspects. This approach is extended to concurrent and communicating systems by the use of a synchronous product of STSs. We proved that the STS is an abstract interpretation of the generated specification. We demonstrate that the set of axiom may be transformed into a terminating term rewriting system. Then from the generation method of the specification the properties of consistency and completeness are got and this ensures the existence of a partial initial algebra. We showed that the synchronous product of GATs preserves the state predicates, the preconditions and the definedness predicate of the components. We also give sufficient conditions to get the GAT determinism and the GAT compactness of the product of two GATs.