Modelling and analysis of evolutionary structures for distributed services
(duration: 09/2006 - 08/2009 /// subsidy: CORDIS FP6)
In open distributed systems, the availability and requirements of components providing services vary over time. The networks need to dynamically reconfigure communication links between components at run-time in a context-aware manner. This reconfiguration includes the (dis)connection of components, but also the adaptation and updating of both components and the network.
Updates may change the computation abilities of components and the coordination abilities of the network. For safety-critical systems, updates should not compromise the reliability of services. Updates should be initiated and effectuated in a decentralized manner.
No formal model of computation and communication exists today in which end-to-end system evolution can be expressed and validated. The use of formal models and validation techniques will significantly improve the confidence in dynamically reconfigurable systems, which are otherwise error-prone.
The CREDO project developed a compositional modeling and validation framework for dynamically evolving software systems, in which computation, coordination and scheduling are clearly separated from each other. We develop a uniform modeling language in which object-oriented components are combined with flexible communication and timing models.
Interface composition enables end-to-end reasoning about evolving systems. These interfaces specify services and formalize the context awareness needed for run-time coordination and reconfiguration. The framework will help developers design and maintain systems by validating reconfigurations. We focus on automatable and compositional validation techniques, including abstract simulation, synthesis, model checking, test-generation, and verification of interface compatibility.
The following tools are used, developed and extended within the CREDO project:
- Eclipse Coordination Tools (ECT) for the modeling of coordination circuitry (REO circuits and Constraint Automata) and for transformation and code generation;
- CREOL Platform (CP) for the modeling and simulation of component internals in terms of the CREOL OO modeling language;
- Testing Tool Suite (TTS) for the testing of component models and for checking the conformance between component behavioral interfaces and implementation classes;
- UPPAAL for performing schedulability analysis of CREOL models.
The usefulness of the framework is assessed through two case studies, one of these being carried out by Almende. The focus of Almende is on applying these tools and techniques to the ASK system, an intelligent communication platform developed by Almende and marketed by spin-off company ASK Community Systems. We focus on two aspects of ASK:
- Modeling the ABBEY (the multithreading component of ASK) task handling infrastructure and analyzing its schedulability;
- Expressing coordination issues in the ASK core components.
CREDO website of project coordinator CWI
CREDO factsheet of Cordis FP6