Research

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 project. 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.

The intrinsic concurrent nature of interactions among software entities is the root cause of the sheer complexity of the resulting systems. Indeed, in order to analyse the behaviour of such a system, one has to consider all possible interleavings of the operations executed by its components. Thus, the complexity of software systems is exponential in the number of their semantics-preserving, making a posteriori verification of their correctness practically infeasible. An alternative approach consists in ensuring correctness by construction, through the application of well-defined design principles, imposing behavioural contracts on individual components and by applying automatic transformations to obtain executable code from formally defined high-level models.

The term “Rigorous System Design” (RSD) denotes the design approach that is based on a formal, accountable and iterative process for deriving trustworthy and optimised implementations from models of application software, its execution platform and its external environment. A system implementation is derived from a set of appropriate high-level models by applying a sequence of semantics-preserving transformations. An instance of the RSD flow is shown in the figure below.

A simplified instantiation of the Rigorous System Design flow

It involves four essential steps:

  1. A high-level, functional application model is defined based on the relevant user requirements, specifications of the functional behaviour of system components and coordination constraints imposed on their interaction.
    At this stage, behavioural properties, such as deadlock-freedom, can be established by analysing component interactions.
  2. An abstract system model is obtained by combining the application model defined in the previous step with a model of the execution platform architecture and a mapping between application and platform components.
    At this stage, performance can be evaluated by simulation based on the characteristics of the execution platform components.
  3. A concrete system model is obtained by model transformation from the abstract system model, incorporating platform-specific communication primitives. Typically, at this stage, high-level interaction mechanisms are replaced by appropriate primitives provided by the execution platform, e.g. message passing or shared memory regions.
  4. Finally, executable code is separately generated for each processing element of the target platform.

The RSD approach has a number of advantages over conventional design processes. In particular:

  • All relevant concerns are strongly separated, each being specified using a dedicated model in a suitable formalism.
  • Design decisions are only taken when strictly necessary, ensuring that all design space restrictions are justified and traceable to clearly stated requirements, expressed in languages or formalisms with clear semantics.
  • Properties established at any step of the design flow are preserved throughout the subsequent steps including the executable implementation. Thus resulting systems are correct by construction.

My current research objective is to develop methods and tools for the rigorous design of distributed self-adaptive software systems, which can be proven to be correct by construction. The primary application domain is the development of cloud computing platforms and applications.