Component-Based Modeling, Analysis and Animation

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. The model-based approach and analysis and animation techniques will be described and demonstrated through a series of examples and using the Labelled Transition System Analyser (LTSA) toolkit, which has been extended to deal with animation and MSCs