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. In order to facilitate model construction early in the design process, the behaviour models can be synthesised from scenarios, captured as message sequence charts (MSC). Models described in this way can be used as an initial basis for validating requirements and as a specification that must be satisfied by more detailed models. By using a model-based design process early in the software lifecycle we hope that users gain the greatest benefit from model building and analysis. By providing techniques to generate models from scenarios and by associating the models with the proposed software architecture, we embed modeling into the software process. The ability to associate animation with models provides an accessible means for interpreting both model behavior and misbehavior to users. Analysis and animation can be carried out at any level of the architecture. Consequently, component models can be designed and debugged before composing them into larger systems. 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.