New formal methods for software reconfiguration in cloud computing

Publication date: 29-06-2011

The complexity of today’s software poses new requirements on the design and analysis of computer systems. In service-oriented computing and cloud computing, applications use and integrate software from third-party providers, distributed over the internet. If software needs a service that fails or responds slowly, it can be automatically adapted with dynamic reconfiguration. Christian Krause, PhD student from the Centrum Wiskunde & Informatica (CWI) in Amsterdam, developed new techniques for dynamic software reconfiguration. On 21 June he defended his thesis ‘Reconfigurable Component Connectors’ at Leiden University. His research can be applied in service-oriented and embedded systems, for example in the automotive industry.

Safer and faster

In safety-critical systems, the quality of dynamic reconfigurations is vital. In modern cars, for example, hundreds of electronic controller units must operate in different modes, depending on the current situation – such as driving on a highway or finding a parking spot. Switching between these modes is a typical example of dynamic reconfiguration. Performing a dynamic reconfiguration on the running system must preserve the consistency of the states of its components before, during and after the reconfiguration. Formal methods can ensure that a reconfiguration does not have any safety-critical side effects – for example, that changing the air conditioning temperature does not influence the functioning of the brakes. Formal methods not only make the software safer, but also make it possible to run the applications faster.

Krause used the coordination language Reo for modelling and formal analysis of dynamic software reconfiguration. He applied different types of formal methods, such as graph transformation and model checking, to reason about dynamically changing component connectors: software which integrates and orchestrates distributed, heterogeneous components and services. To apply his techniques in practice, Krause developed the Extensible Coordination Tools (ECT), a set of Eclipse plug-ins providing an integrated, graphical environment for modelling and analysis of component connectors in Reo. This open source tool is based on the Eclipse platform and can be obtained freely from This research is part of the Software as Service research theme, one of CWI’s research highlights.


More information:

- PhD thesis:
- Supervisor: Prof. dr. F. Arbab (CWI and Leiden University). Cosupervisor: dr. E.P. de Vink (Eindhoven University of Technology).
- This research has been carried out at the Centrum Wiskunde & Informatica (CWI), under the auspices of the research school IPA (Institute for Programming research and Algorithmics). It was funded by the NWO GLANCE project Workflow Management for Large Parallel and Distributed Applications (WoMaLaPaDiA).
- Picture: Ellen Mahi.