Our group is regularly involved with many research projects sponsored by the European Community (EC), Italian Ministry of University and Research (MIUR), National Council of Research (CNR), National Body for Alternative Energies (ENEA).

Here is a selected list of them.

WFR

Web Fitting Room (MSE project).

This is a project sponsored by MSE (Ministero dello Svilluppo Economico) in the "Industria 2015" framework. WFR goal is to design and implement on demand production of fashion clothes by connecting a web based fitting room (where clothes are virtually fitted) to a beyond-state-of-the art Decision Support System (DSS) that will drive on-demand production of the selected clothes. Our role in this project is in the design and implementation of such DSS by using model checking based techniques to overcome the limitations of currently available DSS technology.

ESA ITI AO6067

Model Checker Validator for Satellite Operational Procedure.

The goal of this ESA Innovation Triangle Initiative (ITI) is the design and implementation of a novel model checker that, interacting with ESA satellite simulators, can support Verification and Validation (V&V) of satellite operational procedures. Prime contractor and end user: Telespazio.

ULISSE

USOCs KnowLedge Integration and Dissemination for Space Science Experimentation. (EC FP7).

Our role in this project is in the design of model checking algorithms for automatic verification of on board procedures.

ESA 5459

System and Software Functional Requirements Techniques.

Our role in this project is the investigation of model checking techniques for system level analysis starting from a SysML definition of requirements and of the system itself.

INTERCEPTOR

Motion Planning with moving obstacles (INTECS).

This is an industrial project fully supported by INTECS. Our role in this project is that of designing model checking based algorithms for motion planning in presence of moving obstacles.

SINTESI

Advanced Sense and Respond System (MIUR project).

Our role in this project is that of designing model checking based algorithms for the automatic synthesis of reaction rules in SaR (Sense and Respond) systems for automatic resource allocation in multimedia enterprises.

SAPP

Advanced System for Fault Tolerant Design of Wireless Networks (FILAS project).

Our role in this project is that of designing model checking based algorithms for the optimal and fault tolerant positioning of relays nodes in a wireless network.

CRESCO

Vulnerability Analysis of Complex Systems (MIUR project).

Our role in this project, as consultant, is that of designing model checking based algorithms for the vulnerability analysis of telecommunication networks to malicious attacks.

TRAMP

An Integrated Control and Management System for the Safe Transport of Dangerous Goods (MIUR project).

This project goal is to increase the safety of the transport of dangerous goods by using Information Technology. Safety of the all system heavily depends on the application layer protocols used for communication between the vehicles and the control centre that is monitoring them. Our role in this project is to use model checking techniques for the verification of the whole system safety as it depends on the application layer protocols.

IRRIIS

Integrated Risk Reduction of Information-based Infrastructure Systems (EC project).

This project goal is that of investigating risk reduction techniques for large critical infrastructure systems (LCCIs). As an ENEA consultant our involvement in this project has been that of designing a MILP (Mixed Integer Linear Programming) based tool to minimize inoperability in a complex infrastructure.

SETRAM

A Logistic Expert System for the Optimisation of Multimodal Freight Transportation (MIUR project).

This project goal is to investigate multimodal optimisation on large real world freight transportation systems. As an ENEA consultant our involvement in this project has been twofold: 1. Interfacing heuristic search based optimisation algorithms with the logistic DB in a J2EE frame; 2. Investigate optimisation algorithms working directly on the logistic DB.

SAFEGUARD

Intelligent Agents Organization to Enhance Dependability and Survivability of Large Complex Critical Infrastructure (EC project).

The goal of this project is to investigate techniques to enhance dependability and survivability of complex systems. The target infrastructure has been a telecommunication network. As an ENEA consultant our involvement in this project has been that of designing and implementing a TCP anomaly detection tool based on Markov Chains.

SAFE TUNNEL

Safe Tunnel (EC project).

The goal of this project is that of investigate techniques to increase safety inside Alpine tunnels. Basically this project investigates the possibility of using a control centre to send suitable advise/commands to the vehicles inside the tunnel. Safety of the whole system of course depends on the interaction between the system components and the application layer protocols used for communication between the vehicles and the control centre. As an ENEA consultant our involvement in this project has been on the verification of such application layer protocols using model checking techniques.

MEFISTO

Formal Methods for Security and Time (MIUR project).

The goal of this project is that of investigating how formal methods can be used to check security of systems in which time plays a relevant role. Our role in this project is that of improving the state of the art on algorithms and tools for the verification of probabilistic protocols and hybrid systems.

ICARO

ICARO (MIUR Project).

The goal of this project is to devise methods and tools for the reliability analysis of complex hybrid systems such as the ICARO cogenerative plant at ENEA Casaccia (Italy). As an ENEA consultant our involvement in this project is that of modelling and verifying the ICARO control system using state of the art model checking techniques.

TOSCA

Theory of Concurrency, Higher Order Languages and Types (MIUR project).

The goal of this project is that of investigating how formal methods can be used to check properties of concurrent systems both statically and dynamically. Our role in this project is that of devising improving the state of the art on model checking algorithms and tools for verification of concurrent system.