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
- Modelling language
We develop a modelling language based on
updatable components and reconfigurable networks composable through
service interfaces.
- Type checking
We develop type systems that restrict the
dynamic reconfiguration of Credo models such that their type-safe
execution can be guaranteed by static analysis.
- Extended static checking
Dynamic properties of the
service interfaces expressed by assertions will be statically
analysed using automated verification techniques based on semantic
tableaux.
- Model-checking
The generic verification engine (UPPAAL)
is used to model-check timing and resource requirements of the
specification of the component interfaces by automata.
- Simulation and testing
A high-level implementation of the
Credo language in the rewrite logic of the Maude tool is used to
test components using a high-level simulation language to drive the
execution. As the computational model does not commit to a
particular scheduling strategy, scheduling is orthogonal to the
functional properties of components, and experiments expressed in
the high-level simulation language may be conducted with different
local schedulers. Scheduling strategies also apply to the network.