Formal Methods && Tools Group

Current and Recent Projects

  • STINGRAY : SmarT INtelliGent RAilwaY. ECM, an industry leader in high-speed rail control system is the project coordinator. Participate as research bodies: FMT LAB (ISTI-CNR) DINFO of UNIFI (POR FESR Toscana 2014-2020 ASSE 1 - AZIONE 1.1.5 – Sub-azione a1 “Progetti strategici di ricerca e sviluppo“ (Bando 1) - Decreto 24.05.2017 n. 7165, cofounded by Tuscany Region).
  • ASTRail: SAtellite-based Signalling and Automation SysTems on Railways along with Formal Method and Moving Block validation.
    The ASTRail project falls within the scope of the topic S2R-OC-IP2-01-2017, Operational conditions of the signalling and automation systems signalling system hazard analysis and GNSS SIS characterization along with Formal Method application in railway field, which is connected with the complementary topics S2R-CFM-IP2-01-2015 and S2R-CFMIP2-01-2017.The ASTRail project will act to enhance the signalling and automation system by searching innovative solutions that exploit cutting edge technologies already present in sectors different from the rail such as the avionics or the automotive sector. Investigation of such technologies and assessment of their reusability in the railway field will be done taking in particular care all issues related to safety and performance in the rail system.
  • 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).
  • 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.
  • 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

  • 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.
  • Ascens: Autonomic service-component ensembles (FP7 IST PROGRAMME IST, 2010-2014)
  • 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)