Formal Methods && Tools Group

Current Projects

  • TRACE-IT: Train Control Enhancement via Information Technology. ECM, an industry leader in high-speed rail control system is the project coordinator. Participate as research bodies: FMT LAB (ISTI-CNR) DIEF and DISIT-DSI of UNIFI (PAR FAS 2007-2013 Azione 1.1 P.I.R. 1.1.B, 2011-2013, cofounded by Tuscany Region).
  • Ascens: Autonomic service-component ensembles (FP7 IST PROGRAMME IST, 2010-2014)
  • Quanticol: A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours “QUANTICOL” is a European research initiative involving the University of Edinburgh, Scotland; Istituto di Scienza e Tecnologie della Informazione “A. Faedo”, Italy; Ludwig-Maximilians-Universität München, Germany; Ecole Polytechnique Fédérale de Lausanne, Switzerland; and IMT Lucca, Italy.
  • CINA: Compositionality, Interaction, Negotiation, Autonomicity (A MIUR PRIN project) The project deals with the issues related to the development and management of open-ended IT systems consisting of heterogeneous, highly parallel, massively distributed components with complex interactions and behaviours and with autonomy in terms of individual properties, objectives and decision-making. It aims at developping a coherent, integrated set of languages, methods and tools to build systems that can operate in open-ended, unpredictable environments while adapting to changing contexts or requirements, and that behave reliably and are able to cope with failures and attacks.
  • LearnPad: (Model-Based Social Learning for Public Administrations) The project will build an innovative holistic e-learning platform for PAs that enables process-driven learning and fosters cooperation and knowledge-sharing. The platform supports both an informative learning approach based on enriched business process (BP) models, and a procedural learning approach based on simulation and monitoring (learning by doing). Formal verification and natural language processing techniques will ensure quality of the content and the documentation.

Former Projects

  • SENSORIA: Software Engineering for Service-Oriented Overlay Computers (FP6-2004-IST-FETPI)
  • TOCAI.IT: Knowledge-oriented technologies for enterprise aggregation in Internet (FIRB-MIUR)
  • FAERUS: Formal Analysis of Evolving Resilient Usable Systems, International mini-project in the context of the EU Network of Excellence ReSIST, 2008
  • XXL: Sviluppo di nuovi strumenti e tecniche per lo specifica e verifica formale di sistemi ad elevata granularità (Advanced Tools and Techniques for the Specification and Verification of Systems with Elevated Granularity), CNR-RSTL (Ricerca Spontanea a Tema Libero) project, 2008-2009
  • D-ASAP: Architetture Software Adattabili e Affidabili per Sistemi Pervasivi
  • MOD-CONTROL: Train control and monitoring system, a sub-project of MODTRAIN (FP6-PLT-506652/TIP3-CT-2003-506652).
  • PaCo: Performability-Aware Computing: Logics, Models, and Languages. Italian National Scientific Research Programme. Call published with D.M. 1175 del 18/09/2007 (PRIN 2007). Approved with nota 95 of 23/07/2008. September 2008 - August 2010.

The FM&&T group has participated to the following projects

  • AGILE: Architectures for Mobility Information Societies Technology (IST PROGRAMME IST-2001-32747, 2002-2004)
  • CAFE: IT EUREKA Project “Information Technology for European Advancement” (ITEA, 2001-2003)
  • PRIDE: ambiente di PRogettazione Integrato per sistemi DEpendable (Italian Space Agency, 2002)
  • TACIT: Theory and Application of Continuous Interaction Techniques (EU-TMR, 1998 - 2002)
  • Architetture Software ad Alta Qualita’ di Servizio per Global Computing su Cooperative Wide Area Networks High-Quality Service Software Architectures for Global Computing on Co-operative Wide Area Networks (MURST 5%)
  • DIMMIBENE (CNR Agenzia 2000)
  • La prossima generazione di sistemi di trading on line: Aspetti relativi la sicurezza The next generation of trading-on-line systems: Problems related to security (CNR Agenzia 2000)
  • QUACK: A Platform for the Quality of New Generation Integrated Embedded Systems (Progetto MURST 40%)
  • CNR GMD: Formal test cases derivation for UML Statechart Diagram specification (CNR Bilateral project, 1999 - 2001)
  • HIDE: EU ESPRIT Project 27439 “High-level Integrated Design Environment for Dependability”, 1998
  • QESDSPM CNR Trilateral Project (CNUCE, IT; Univ. Twente, NL; Univ. Erlangen-Nurnberg, D) “Quantitative Event Structures, Discrete Simulation and Performance Modeling”, 1997-1999
  • GUARDS: (Fourth Framework Programme,1996 -1998).
  • IRS: Interactionally Rich Systems e Interactionally Rich Immersive Systems (EU-HCM, 1993 -1997)
  • AMODEUS: (EU Basic Research Action 7040, 1992-1995)