Component-based software construction is widely used in a variety of applications, from embedded environments to grid computing. However, errors in these applications and systems may have severe financial implications or may even be life threatening. A rigorous software engineering approach is necessary. We advocate a model-based tool-supported approach to the design of concurrent component-based systems. Component behaviour is modeled as a finite state process and specified in a process algebra FSP. In the same way that components can be composed according to an architecture so as to provide (sub-)system functionality, so component models can be composed to construct a system behaviour model. These models can be analysed using model checking against required properties specified in FSP or Linear Temporal Logic. Furthermore, these models can be animated to demonstrate and validate their behaviour and to replay counterexamples to illustrate their misbehaviour. In order to facilitate mo...