Objective

The objective of this project is the development and application of an integrated suite of tools for compositional modelling, testing, and validation of software for evolving networks of dynamically reconfigurable components.

Case studies

The ASK system is a system for connecting people to other people or for automated response systems (e.g., interactive voice response IVR). The specific problem of this case study, addressed by this project, is to model and verify specific dynamically reconfigurable parts of the complete system using the compositional modelling and verification techniques developed in this project, in the setting of the services provided by other preexisting components.

Biomedical sensors are increasingly used to detect abnormal biological changes and monitor biological parameters in tissues and organs. Advanced hospitals are using an array of biomedical sensors for diagnostics, surgical, and post-operative phases. The outcome of this case study is a framework useful for the design of future sensor network solutions, as well as evaluation of their suitability and correctness. The framework will be designed to meet the needs towards better monitoring devices and network solutions.

Approach

The project will develop a new high-level modelling language Credo for the dynamic composition of highly reconfigurable component-based software systems, and light-weight and automated verification techniques and tools supporting this language. Credo integrates a formal component model based on concurrent objects which support run-time updates with a new model of component connectors based on mobile channels. Credo supports rapid prototyping and automated validation of networks of distributed services implemented by components, focusing on analyzing the effect of dynamic reconfiguration. The kernel of the Credo tool suite is an abstract interpreter for the language. The abstract interpreter forms the basis for the development and integration of simulation, testing and validation tools for the compositional analysis of functional, timing, and resource requirements.

The following figure describes the overall architecture of this project in terms of the applications, and tools and techniques for the execution and validation of models in the Credo language. The project will be evaluated by the demonstration of these tools and techniques on the case studies.


The suite of tools and techniques developed or extended in the Credo project includes