Modern software systems are characterized by a shift of focus from the execution of isolated, independent computational units to the interaction between heterogeneous, autonomous, inter-dependent computational units. The objective of the project is the development of a new generation of tools for the description of interacting computational units and of the environments hosting the interactions. Such descriptions should enable developers to pursue static and dynamic forms for software verification aimed at:

  • enforcing safety and liveness properties concerning interactions, such as preventing the exchange of messages with the wrong payload, or ensuring reachability of certain desirable states, such as those denoting the successful completion of an interaction.
  • enabling precise forms of runtime monitoring for untrusted or unreliable components. Such forms of monitoring are instrumental for the dynamic evolution and adaptation of heterogeneous systems.
  • automatically synthesizing adapters for those components and subsystems whose behavior is incompatible as is, but can be adjusted to meet the requirements of the environments in which they need to be executed.

The successful achievement of these objectives has the potential for a deep and broad impact on the practice of software development. The two research groups involved in the project have a longstanding history of research on formal models and particularly on types for both sequential and concurrent programs. The proposed objectives are along the lines of the objectives of the international project COST IC1201 BETTY and Serbian national project ON174026 of the Ministry of Education, Science and Technological Development. It is therefore expected that the coordinated and structured interaction between the two groups will boost research on the topics of the project and contribute to their scientific advances on both sides.