Formalisation of component-based systems

Current advances in software engineering practice involve the adoption of a component-based approach in developing large-scale, complex systems. The component-based paradigm provides better structuring of systems and facilitates systematic software reuse. However, complex interactions between components, especially in concurrent, real-time and embedded applications, pose greater challenges. This thesis proposes a formal language for this kind of systems, especially provides a formal underpinning for the Koala model, for managing the dependencies between components, in terms of their interactions in a concurrent setting. In our model, components are autonomous elements encapsulating functionality and connectors exist only to serve the communication needs of others. Connectors further can initiate and govern component communications. This design takes communication and control out of components and encapsulates them into connectors, hence improves the reusability of components. In our approach, each component is represented by a component signature, which identifies a component; and a timeslot language, which describes the behaviour of a component with timing sensitivity. This language-based representation of component behaviour makes it possible to capture concurrency at the individual interface level. The interpretation of concurrency is that of a non-interleaving model, with the notion of causal independence lifted to multi-threaded runs. Based on time-slot languages as an operational semantic domain, we introduce component protocols, a service-based expression language, serves as a syntactic behaviour description and which can be formally interpreted into time-slot languages via the initial algebra approach. Component interoperability in this approach is a design time concept. It boils down to the properties of deadlock-freedom on glue, loyalty on roles with glue, compatibility of ports and roles, and substitutability between replacement ports and current ports. The well-formedness properties of components and connectors will be evaluated individually before being wired together. These mainly build on the concepts of well-definedness, well-behavedness and refinement relationship of component protocols. This approach follows the practical bottom-up approach from unit-testing to integration-testing.