ACC
ACC is an ongoing project, part of the Strategic Program for Railways research, carried out in collaboration with Rete Ferroviaria Italiana (RFI).
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 that have been developed specifically in the scope of the
projects. The tools are all based on the Eclipse platform: AIDA for the design
of the interlocking system, automatic translation into SysML models and the
generation of executable code and other artefacts like documentation; TOSCA for
the verification by testing and test case generation; NORMA to support the
formalization and the analysis of the legacy relay-based interlocking systems;
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
Start Date: Sep 2018
End Date: Currently running
Budget: 1.9 M€