Database of Case Studies Achieved Using CADP

Coordination of Autonomic Managers in the Cloud

Organisation: Univ. Grenoble Alpes and Inria Grenoble Rhône-Alpes (FRANCE)

Method: LNT

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Cloud Computing.

Period: 2015

Size: 28,992,305 states and 46,761,782 transitions.

Description: Cloud computing allows the delivery of on-demand computing resources over the internet on a pay-for-use basis. From a technical point of view, cloud applications usually consist of several software components deployed on remote virtual machines. Managing such applications is a challenging problem because manual administration is no longer realistic for these complex distributed systems. Thus, autonomic computing is a promising solution for monitoring and updating these applications automatically. This is achieved through the automation of administration functions and the use of control loops called autonomic managers. An autonomic manager observes the environment, detects changes, and reconfigures dynamically the application. Multiple autonomic managers can be deployed in the same system and must make consistent decisions. Using them without coordination may lead to inconsistencies and error-prone situations.

This work presents new synthesis techniques for generating a controller, which aims at coordinating several managers. The generated controller prevents every manager from violating global objectives of all the managers. The proposed controller synthesis techniques assume that all participants (managers and generated controller) interact using asynchronous communication semantics. This means that all the messages transmitted from/to the managers (resp. controller) are stored/consumed into/from FIFO buffers. The approach takes as input a set of autonomic managers, whose behaviours are described formally as Labelled Transition Systems (LTSs). The coordination requirements and interaction constraints are specified using a set of reaction rules and regular expressions. Given a set of manager LTSs and the coordination requirements, the synthesis technique generates an abstract model (LTS) of the controller. The synthesis relies on an encoding of the LTS models and coordination requirements into the LNT language. The generated LTS corresponds to all possible executions of the controller.

Then, once the controller LTS has been synthesized, a specialized code generator translates it into a Java program, which allows one to deploy and use the synthesized controller for coordinating real applications. The overall synthesis approach is illustrated by means of a JEE multi-tier application supervised by two sorts of autonomic managers, namely a self-repair and a self-sizing manager. The application consists of an Apache Web server, a set of replicated Tomcat servers, a MySQL proxy server, and a set of replicated MySQL databases. The Apache server receives incoming requests and distributes them to the replicated Tomcat servers. The Tomcat servers access the database through the MySQL proxy server that distributes the SQL queries to a tier of replicated MySQL databases fairly. To validate the synthesized controller LTS, two liveness properties were formulated in MCL and checked successfully using EVALUATOR.

Conclusions: The proposed synthesis approach covers the whole development process from the expression of the requirements to the final implementation and deployment of the synthesized controller, which helps to coordinate real-world applications at runtime. This study showed that LNT is expressive enough for representing the behaviour of managers, the constraints, and the way they interact together. The synthesis technique proposed can also be used to control applications in other areas (Web services, multi-agent systems, hardware protocols, etc.), where components are modelled as LTSs and communicate asynchronously.

Publications: [Abid-Salaun-dePalma-Gueye-15] R. Abid, G. Salaun, N. de Palma, and S. M. Gueye. "Asynchronous Coordination of Stateful Autonomic Managers in the Cloud". Proceedings of the 12th International Symposium on Formal Aspects of Components and Systems (FACS'2015), Niterói, Brazil, LNCS vol. 9539, pages 48-65. Springer Verlag, October 2015.
Available on-line at:
or from the CADP Web site in PDF or PostScript

[Abid-Salaun-dePalma-17] R. Abid, G. Salaun, and N. de Palma. "Asynchronous Synthesis Techniques for Coordinating Autonomic Managers in the Cloud". Science of Computer Programming 146:87-103, 2017.
Available on-line at:
or from the CADP Web site in PDF or PostScript

Prof. Gwen Salaün
Univ. Grenoble Alpes
Inria and LIG / CONVECS
655, avenue de l'Europe
38330 Montbonnot Saint Martin
Tel: +33 (0)4 76 61 54 28

Further remarks: This case-study, amongst others, is described on the CADP Web site:

Last modified: Thu Feb 11 12:22:05 2021.

Back to the CADP case studies page