MEALS

Mobility between Europe and Argentina applying Logics to Systems

 Partecipanti

Mappa

 Word cloud

Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.

 Obiettivo del progetto (Objective)

'Computing systems are getting ever more ubiquitous, making us dependent on their proper functioning. Therefore we require that they are correct (i.e. they conform their intended behavior), safe (i.e.its operation does not have catastrophic consequences), reliable, available to provide the intended service, and secure (i.e., no user without appropriate clearance can access or modify protected data).

Guarantees for such charcteristics rely on rigid specification and analysis techniques for both the required system functionality as well as its behavior. Formal methods provide a mathematical approach to model, understand, and analyze systems, especially at early development stages.

In this project we focus on three aspects of formal methods: specification, verification, and synthesis. We consider the study of both qualitative behavior and quantitative behavior (extended with probabilistic information). We aim to study formal methods in all their aspects: foundations (their mathematical and logical basis), algorithmic advances (the conceptual basis for software tool support) and practical considerations (tool construction and case studies).

The MEALS project includes five tightly interconnected thematic work packages. They focus on quantitative analysis of concurrent program behaviour (WP1), reasoning tasks for specification and verification (WP2), security and information flow properties (WP3), synthesis in model-based systems engineering (WP4) and foundations for the elaboration and analysis of requirements specifications (WP5).

The crosscutting concern of all these work packages is the development of formal techniques for the specification, verification and synthesis of dependable ubiquitous computing systems. Five carefully planned MEALS gatherings and workshops give the project an effectve structure for knowledge transfer, communitiy building, and result dissemination, aimed at a sustained transcontinental collaboration.'

Introduzione (Teaser)

An EU-funded team is working on tools and methods to formally verify the correct functioning of computer systems under development.

Descrizione progetto (Article)

Inspections, walkthroughs and other reviews aim at ensuring that the results of each step in software development correctly embrace the intentions of the previous step. Testing in the sense of executing the software is only one of multiple techniques used in computer system verification. Systematic computer system verification helps prevent software problems from reaching the production environment.

Researchers working on the 'Mobility between Europe and Argentina applying logics to systems' (http://www.meals-project.eu/ (MEALS)) project propose a mathematical approach to analyse systems at early development stages. Funded under the FP7 'Marie Curie Actions', MEALS has offered Argentinian and European researchers the possibility to jointly carry out their project by exchanging research visits in this four-years programme.

About 100 researchers from 11 scientific and academic institutions joined efforts to formulate advanced methods for formal specifications that help with the development and implementation of computer systems and software. These specifications are "formal" in the sense that they are expressed in a language whose vocabulary, syntax and semantics are formally defined. In other words, the specifications language is based on mathematics.

During the first half of this four-year project, mathematics-based tools and techniques were developed to describe any computer system and aid in its design. These include tools to model and analyse different types of systems, including embedded controllers, distributed systems and web services, in order to study key properties related to functional correctness, security issues, performance profiles, fault tolerance, and many other nowadays indispensable features.

By verifying these key properties through rigorous and effective reasoning tools, it is possible to demonstrate that a system design matches the desired specification. Once completed, the MEALS tools and techniques will allow the revision of incorrect designs before any major investment. The ultimate aim is to extend the industrial use of formal verification techniques and significantly improve the quality of software being developed in the near future.