ACC Projects

ACC is a set of projects, part of the Strategic Program for Railways research, carried out in collaboration with Rete Ferroviaria Italiana (RFI).

ACC is meant to provide domain experts of RFI a structured methodology and a set of usable tools to support the design, traceability, verification and deployment of railways interlocking control systems.

Project details

ACC (“Apparati Centrali Computerizzati”) are computer based railways interlocking control systems.
Railway interlocking systems are safety-critical mechanisms that manage and control train movements across complex track layouts, such as junctions and crossings, to prevent collisions and ensure safe operations. Interlocking systems coordinate signals, points (switches), and other track-based devices so that trains can only proceed when routes are clear and no conflicting movements are possible. They can be mechanical, electrical, or computerized, each employing logical rules to lock specific routes or signals while others are in use. Modern interlocking systems are largely computer-based, allowing for centralized control and integration with automated signaling, enhancing efficiency and safety across railway networks.

Since 2018 FBK has collaborated with RFI within the scope of several projects for a model-based approach to the design, verification and deployment of railway interlocking systems.
In the proposed approach, the flow starts from a set of specifications in Controlled Natural Language (CNL), that are close to the jargon adopted by domain experts, but fully formal. From the CNL, a complete SysML specification is extracted, leveraging various forms of diagrams, and enabling automated code generation. To support the verification process of the interlocking logics, several formal verification methods are supported. A complementary part of the flow supports the extraction of formal properties from legacy interlocking systems designed as relay circuits.

The design and verification process is supported by a comprehensive set of software tools ("OPERA") that have been developed specifically in the scope of the projects. All the tools are based on the Eclipse platform.

  • LUCIA for the formalization of the textual dispositions and regulatory. LUCIA can generate test cases and properties out of the formalized documents.

  • NORMA for the formalization of the legacy relay circuits of the logic. NORMA provides syntactic and semantic checkers of the modeled circuits, and automatically generates test cases and properties with the use of formal method techniques.

  • AIDA for the design of the logic of the interlocking system, automatic translation into SysML models, the generation of executable code and other artifacts like documentation, the execution of test cases and debugging sessions on the generated code in closed loop with a simulator of trains and station devices.

  • TOSCA for the verification by testing and test case generation.

  • CARMEN to support the specification of properties and their verification through formal verification techniques as a complementary approach to testing-based verification.


The tools fully support the flow and are currently used by railway experts to design, verify and deploy several operative systems.

General Info

With a overall budget of ~2.8 M€, ACC is a set of projects started in 2017 and continuing today. Namely, ACC is split into several sequential projects:

  • ACC0: 2017 (3 months)
    • Preliminary assessment, requirements elicitation, project preparation
  • ACC1: 2018-2019 (21 months)
    • Setup methodology
    • Development of AIDA, NORMA, TOSCA
  • ACC2-Toolset: 2022/12 - 2024/04 (16 months)
    • AIDA: extensions to the logic specification language
    • AIDA: profiling and optimization of generated code
  • ACC2-Verifica: 2024/04 - 2025/04
    • LUCIA: methodology and prototype development
    • NORMA: development of algorithms for the analysis of the legacy relay circuits
    • CARMEN: methodology and prototype development
    • TOSCA: extensions of the provided features
  • ACC3-OPERA: 2025/12 - 2028/06 (30 months)
    • Industrialization and integration of the OPERA toolset.
    • Scaling up CARMEN to apply formal verification to the large systems.
    • Implementation of several new features in all tools.

Start Date: Sep 2018
End Date: Jun 2028
Budget: 2.8 M€

Recent Posts