Design of correct-by-construction self-adaptive cloud applications using formal methods

Essentially, any software entity that goes beyond simply computing a certain function necessarily has to interact and share resources with other such entities. Correct coordination of access to resources among concurrent software entities is fundamental to ensuring that they satisfy user and system requirements avoiding operational faults and deadlock situations. This proposal targets the correct coordination of access to cloud resources among concurrent cloud application entities.

Trinh Le Khanh

Trình Lê Khánh is now working on this project


Context

Image by Pete Linforth from Pixabay

Modern software systems are inherently concurrent. They consist of components running simultaneously and sharing access to resources provided by the execution platform. For instance, embedded control software in various domains, ranging from household robotics through operation of smart power-grids to onboard satellite software, commonly comprises, in addition to components responsible for taking the control decisions, a set of components driving the operation of sensing and actuation devices. These components interact through buses, shared memories and message buffers, leading to resource contention and potential deadlocks compromising mission- and safety-critical operations. Similar problems are observed in various kinds of software: system, work-flow management, integration software, as well as cloud computing platforms and applications, which are the main application domain of this proposal. Components of cloud applications interact through cloud resources such as virtual machines, virtual networks, virtual storages, application servers, database managers, middleware services, etc. Thereby, cloud resource sharing can lead to cloud resource contention, potential deadlocks, and operational faults.

Essentially, any software entity that goes beyond simply computing a certain function necessarily has to interact and share resources with other such entities. Correct coordination of access to resources among concurrent software entities is fundamental to ensuring that they satisfy user and system requirements avoiding operational faults and deadlock situations. This proposal targets the correct coordination of access to cloud resources among concurrent cloud application entities.

Host laboratory

Spirals (Self-adaptation for distributed services and large software systems) is a project-team at Inria Lille –Nord Europe research centre. Its research program focuses on defining self-adaptive distributed software services and systems. In particular, one of the two key properties that it targets is self-optimisation, i.e. the capability of systems to continuously reason about themselves and to take appropriate decisions and actions on the optimisations they can apply to improve their usage of the available resources. In order to provide this capability, Spirals is conducting a study of mechanisms for monitoring, taking decisions, and automatically reconfiguring software at run-time and at various scales.

In the domain of (multi-)cloud computing, Spirals researchers study both platform (re)configuration and application design. Both aspects involve complex concurrent software systems, which must be capable of self-adaptation while ensuring correctness in spite of subtle dependencies both among the software components and between components and the resources provided by the execution platforms. Thus, this proposal targets the design of cloud applications, which are both correct-by-construction and self-adaptive, using formal methods.

The work on multi-cloud application design is structured around OCCIware—a model-driven cloud resource management framework [5] based on the Open Cloud Computing Interface (OCCI) standard, providing a unique and unified framework to manage OCCI artefacts (documents, specifications, models, code and tools) and, at the same time, representing a factory to build domain-specific modeling frameworks for cloud computing, where each framework targets a specific cloud domain, such as infrastructure management, container management, application management, elasticity management, etc.

Proposed research project

The OCCIware modelling framework provides a means for specifying the behaviour associated to OCCI entities as a Finite State Machine (FSM). Although such FSMs can be used to monitor and coordinate the behaviour of the corresponding entities, no such mechanisms are currently available. The first step of the project will consist in extending OCCIware with coordination capabilities using JavaBIP [3], an open-source Java implementation of the BIP (Behaviour-Interaction-Priority) framework [2, 4] for the coordination of concurrent components, relying on annotations, component APIs and external specification files.

Currently, FSM specifications in OCCIware are available for elements of the cloud infrastructure such as virtual machines/networks/storages and of the cloud application such as databases, etc. This allows, in particular, to guide cloud application deployment w.r.t. available cloud resources. Once the application is deployed, there is little control of its resource use and requirements. In order to safely manage these at runtime, allowing the applications to dynamically adapt their behaviour to the changes in cloud resource availabilities, FSM specifications of these applications must also be provided. The second step of the project will consist in defining an easy-to-learn intuitive domain-specific language (DSL) to allow developers to provide these specifications and integrating them into the overall model of the cloud system.

In order to ensure acceptance of the project results by software developers, one has to minimise the effort, which they must put into providing additional specifications. The third step of the project will consist of developing algorithms and infrastructure for learning an FSM model of a cloud application by interacting with it and observing its execution traces [1].

Partnership and collaboration

The results of this research project, i.e.

  1. the integration of JavaBIP into OCCIware,
  2. the DSL to specify cloud application self-adaptiveness,
  3. learning algorithms and infrastructure,

will be validated against cloud applications provided by three of Spirals partners: XScalibur, Scalair, and Orange Lab. XScalibur is a spin-off company originating from Spirals, which develops and markets the Multi-Cloud Studio—a product based on the OCCIware framework—for automatisation and administration of virtualised resources provided by heterogeneous cloud computing platforms. Scalair, a regional cloud architect and operator, is our partner in the CIRRUS joint-team. Our partner Orange Labs will bring us applications from the domain of Network Virtualisation Functions (NFV), which consists of the cloudification of network functions.

Estimated work plan

  • M0-M6 – State of the art on the correct coordination of concurrent cloud resources and cloud applications.
    Milestone 1: Submission of this SotA to a top-level review (e.g. ACM Computing Surveys).
  • M6-M12 – Integration of JavaBIP inside OCCIware (i.e. first step), and validation against partner’s applications.
    Milestone 2: Submission of an international conference paper (e.g. IEEE CLOUD).
  • M12-M18 – Design and implementation of the cloud application self-adaptiveness specification language (i.e. second step), and validation against partner’s applications.
    Milestone 3: Submission of an international conference paper (e.g. COORDINATION).
  • M18-M24 – Design and implementation of learning algorithms and infrastructure (i.e. third step), and validation against partner’s applications.
    Milestone 4: Submission of an international conference paper (e.g. ICML).
  • M24-M30 – Integration of the three steps, and validation against partner’s applications.
    Milestone 5: Submission of a top-level review article (e.g. IEEE TCC).
  • M30-M36 – Preparation of the manuscript.
    Milestone 6: PhD thesis defence.

Required skills

The following skills are required for this project:

  • Knowledge of cloud computing
  • Basics of formal methods (e.g. automata, predicate logics)
  • Proficiency in the Java programming language
  • Fluent English (both speaking and writing)

The following skills are not required, but could constitute a plus:

  • Advanced knowledge of formal methods (e.g. temporal logics)
  • Constraint programming

References

  1. Dana Angluin (1987): Learning regular sets from queries and counterexamples. Information and Computation 75(2), pp. 87–106.
  2. Ananda Basu, Saddek Bensalem, Marius Bozga, Jacques Combaz, Mohamad Jaber, Thanh-Hung Nguyen & Joseph Sifakis (2011): Rigorous Component-Based System Design Using the BIP Framework. IEEE Software 28(3), pp. 41–48.
  3. Simon Bliudze, Anastasia Mavridou, Radoslaw Szymanek & Alina Zolotukhina (2017): Exogenous coordination of concurrent software components with JavaBIP. Software: Practice and Experience 47(11), pp. 1801–1836.
  4. Simon Bliudze & Joseph Sifakis (2007): The Algebra of Connectors — Structuring Interaction in BIP. In: Proceedings of the EMSOFT’07, ACM SigBED, Salzburg, Austria, pp. 11–20.
  5. Faiez Zalila, Stéphanie Challita & Philippe Merle (2019): Model-Driven Cloud Resource Management with OCCIware. Future Generation Computer Systems. To appear.