Tronci

Enrico Tronci

Position: 
Associate Professor
phone: 
+39 06 4991 8361
Personal site: 
http://mclab.di.uniroma1.it

Short Biography: 

Enrico Tronci is currently an Associate Professor with the Computer Science Department of the University of Roma ``La Sapienza'' (Italy).
From 1994 to 2000 he has been a Researcher with the Computer Science Department of the University of L'Aquila (Italy). From 1992 to 1993 he has been a Post-Doc at LIP (Laboratoire pour l'Informatique du Parallelisme) at the ENS (Ecole Normal Superior) of Lyon (France).
In 1991, under the supervision of Prof. Richard Statman, he received his Ph.D. degree from Carnegie Mellon University, Pittsburgh, USA.
In 1987, under the supervision of Prof. Corrado Boehm and Prof. Giorgio Ausiello, he received his Master degree in Electrical Engineering from the University
of Roma ``La Sapienza'' (Italy).

His research activity focuses on model checking based algorithms and tools for the automatic verification and synthesis of reactive mission critical or safety critical cyber-physical systems.

He has served as conference chair, member of the program committee or as a reviewer in many conferences and journals. He has authored more than fifty scientific papers on international journals and conferences and is regularly involved in National as well as International research projects funded by the Europena Community (FP7) as well as by the European Space Agency (ESA).

Projects list: 
  • ESA ITI AO6067 - 2010 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 SIMSAT, can support automatic formal Verification of satellite operational procedures. Inventor: UNIROMA1; developer, end-user and prime contractor: TELESPAZIO.
  • Web Fitting Room (MSE) - 2010 Web Fitting Room (WFR) is a project sponsored by MSE (Ministry of Economic Development) 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.
  • ULISSE (EC FP7) - 2009 USOCs KnowLedge Integration and Dissemination for Space Science Experimentation. Our role in this project is in the design of model checking algorithms for automatic verification of on board procedures.
  • ESA 5459 SSFRT - 2008 System and Software Functional Requirements Techniques. Our role in this project is the investigation of model checking techniques for hybrid systems for verification of requirements of level analysis starting from a SysML definition of requirements and of the system itself.
  • INTERCEPTOR (INTECS) - 2008 Motion Planning with moving obstacles. 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 (MIUR) - 2008 Advanced Sense and Respond System. 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 (FILAS) - 2008 Advanced System for Fault Tolerant Design of Wireless Networks. 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 (MIUR) - 2007 Vulnerability Analysis of Complex Systems. 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 (MIUR) - 2007 An Integrated Control and Management System for the Safe Transport of Dangerous Goods. 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.
  • SETRAM (MIUR - ENEA) - 2006 A Logistic Expert System for the Optimisation of Multimodal Freight Transportation. 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.
  • IRRIIS (EC FP6 - ENEA) - 2005 Integrated Risk Reduction of Information-based Infrastructure Systems. 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 is that of designing a MILP (Mixed Integer Linear Programming) based tool to minimize inoperability in a complex infrastructure.
  • SAFEGUARD (EC - ENEA) - 2004 Intelligent Agents Organization to  Enhance Dependability and  Survivability  of Large Complex Critical  Infrastructure. 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 (EC - ENEA) - 2003 Innovative Systems and Frameworks for Enhancing of Traffic Safety in Road Tunnels. 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 (MIUR) - 2002 Formal Methods for Security and Time. 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 (ENEA) - 2001. 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 (MIUR) - 2000 Theory of Concurrency, Higher Order Languages and Types. 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.