Formal specifications are now widely accepted in software development. Recently, he need for a separation of concerns with reference to static and dynamic aspects appeared. Furthermore, in order to be able to design complex architectures and communication patterns, we need a structured approach which allows us to decompose a system in to subparts and to recompose is from them. Finally, a notion of formal reusable component which is suitable to describe both functional and dynamic aspects is also required.

This paper presents the Korrigan model. It allows one to specify in a uniform and structured way both datatypes and behaviours using Symbolic Transition Systems and algebraic specifications. We demonstrate its ability to describe reusable components in a formal way with well defined interfaces. We also demons rate hat Korrigan is relevant to describe the architecture and communication schemes of systems hat may present a complex structure.