Formal Methods for the Development and Evaluation of Sustainable Systems

Project facts

Project promoter:
Complutense University of Madrid
Project Number:
ES07-0014
Target groups
Researchers or scientists
Status:
Completed
Initial project cost:
€100,050
Final project cost:
€98,378
From EEA Grants:
€ 98,378
The project is carried out in:
Spain

Description

The increasing complexity of our computer based systems makes crucial to adopt high standards of quality in their development and validation. Sometimes these systems are not initially faulty, but their unexpected or malicious use or any malfunction after their use cause those problems. The objective of the project is establishing the foundations to state at which extent a system robustly satisfies its specification: a distance will indicate how far away a correct system is from failing the last. They will define logic to state those robustness properties, and sketch a methodology that will produce systems whose robustness could be precisely defined and formally checked. Computer based systems are everywhere in modern society. In light of the increasing complexity of such computing devices, and of the fact that they control important, when not critical, operations, it is crucial to adopt high standards of quality in their development and validation. The project can benefit society as a whole.The expertise of the two leaders of the Icelandic group will provide the mature reflections that will contribute to achieve the defined goals.

Summary of project results

During the project, and also before and after it, partners have been working together in most of the topics included in the project presentation. In particular, they have investigated the modal logics which allows to define the kinds of distance between processes in which they were interested. These include the consideration of modal transition systems and interface theories. Moreover, they have also consider the complex interval logics, in which Dario Della Monica is a big expert. Some smaller efforts were devoted to the contribution of the development of automatic tools which allow the analysis of systems, such as TAPAAL. Ignacio Fábregas (UCM) is now totally integrated in Luca Aceto’s group (RU), and has started to study the so called nominal systems, where possible partners will be able to introduce their distances in the future. One of the important tasks performed by the project coordinators David de Frutos (UCM) and Luca Aceto (RU) has been the organization and celebration of the International CONCUR Conference and other important satellite events. The enormous prestige of this Conference attracts each year a big number of collocated events that the organizers commit to organize after filtering them. In this occasion there were 11 different events, and proceedings shall be published by an important company. Later in Reykjavik they did the same for the 27th Nordic Workshop on Programming Theory (NWPT 2015), close to the end of the project; they gave talks at the seminars of the other institution and participated in the technical discussions of local groups when visiting. Some totally tangible fruits of the project come from the organization of such conferences, in the form of scientific publications. At least 14 papers have been prepared, some of them published, others submitted and others still in preparation. Partners expect that the results of the research made shall be published and mostly made immediately available to the international community through open publication. They will contribute to develop the new approaches to the measurement of the quality of systems, and will enlight not only those promising paths to follow, but also the already explored ways that instead have exhibited serious difficulties that probably will be better to elude, or at least postpone at the moment.

Summary of bilateral results

The organization of the CONCUR Conference, in which both coordinator researchers where nominated Co-chairs, and its satellite events was a great opportunity to disseminate and to give high visibility to the work of involved teams. Partners expect to continue their close collaboration in the future, looking for funding that will make possible to cover the expenses of exchanges and stays of researchers of both teams at the partner institution. According to the project coordinator, the privilege of having the opportunity to collaborate with one of the main international experts in the field of Theory of Concurrency, by also one of the crucial names in the whole field of Theoretical Computer Science, as proves the fact that Luca Aceto is currently the President of the European Association of Theoretical Computer Science, is extremely valuable. The youngest members of both groups have been the most benefitted by the project funding: Ignacio Fábregas and Dario Della Monica had great opportunities as Postdocs, while David Romero and María Martos used their stays to support the International special recognition of their PhD Thesis.