Behavioural approach to modular system specification

Abstract

The algebraic approach to modular specifications as developed by the first author during the last five years is joined with the behavioural approach to algebraic specifications introduced recently by the last two authors. In the joint approach module specifications are provided with a behavioural functorial semantics. As main results we show that basic interconnection mechanisms, like composition, union and actualization are correctness preserving and compositional w.r.t the behavioural semantics. In practice also the case of view actualization is of great interest where non observable actual sorts can be bound to observable formal sorts. Also in this case, which requires behavioural view functors instead of forgetful functors, we discuss how to extend the basic constructions and results. Most constructions and results are illustrated by a behavioural module specification of a modular airport schedule system.