A type language for distributed reactive components governed by communication protocols

Component based software engineering (CBSE) is a methodology that aims to design and build software systems by assembling together reusable and loosely coupled components. Applying CBSE in a distributed setting is appealing but challenging: distributed applications require different remote components to interact following a well-defined protocol. In this paper we consider a model for message passing component-based systems where components are assembled together with a protocol, and are reactive to messages in a flexible way. We propose a type language that allows capturing component reactive behaviour and checking its compatibility with the protocol. Moreover, we show the correspondence of component and type behaviours, which entails a progress property for components.