Nel contesto del sistema Communications-based Train Control (CBTC), l’ISTI si è concentrato sul sotto-sistema ATS (Automatic Train Supervision).

Il CBTC è un’innovativo sistema di controllo automatico del traffico ferroviario
metropolitano, che fornisce una protezione continua e automatica dei treni, permettendo di aumentarne prestazioni e disponibilità.

Di seguito sono descritte le principali funzioni allocate a ATS, facendo riferimento alla figura sopra:

• le Tabelle Orario (1) corrispondono all’orario ferroviario di servizio. Sono generate periodicamente, ad esempio a cadenza semestrale per una determinata linea e contengono le informazioni necessarie per stabilire il profilo di missione di ciascun treno rispetto al servizio, ovvero gli orari di arrivo e partenza da ciascuna stazione, il binario da utilizzare nella stazione, le fermate di servizio.
•  ATS fornisce a ciascun treno (SSB ATO) il profilo di missione (2) prima dell’inizio della missione.
•  ATS conosce la posizione di ciascun treno in base alle informazioni (3) che riceve dal sottosistema ATP/ATC. In base al profilo di missione, in un momento opportuno richiede (4) all’interlocking (IXL) l’assegnamento di un itinerario, ad esempio per portarsi dalla linea al binario su cui dovrà essere effettuata la fermata.
• Si noti che IXL può solo determinare se l’itinerario è assegnabile rispetto allo stato di occupazione dei binari, ma qualora esso non sia attuabile a causa dei vincoli di segnalamento (o di un degrado) non è in grado di assegnare autonomamente un itinerario alternativo (p. es. dalla linea a un binario diverso). Questa funzione è a carico di ATS. Si deve prevedere quindi una conferma dell’assegnamento dell’itinerario (5).
• Si  ipotizza che tutta l’infrastruttura sia gestita da un unico IXL centralizzato (p. es. un ACC) che è il caso più usuale in un sistema CBTC.

Meccanismi di prevenzione di deadlock (stallo): Il sistema contiene due meccanismi per evitare il verificarsi di situazioni di stallo, dove due o più treni non possono procedere perché in attesa l’uno dell’altro.

• Il meccanismo Aree Critiche si basa su un file di configurazione AreeCritiche.xml che contiene la struttura delle sezioni di linea dove si possono verificare deadlock e un insieme di regole di scheduling da seguire. La validazione del file di configurazione è effettuata attraverso tecniche di Model Checking.
• Il meccanismo Liveness evita deadlock basandosi solo sull’analisi dinamica dello stato del sistema a costo di un maggiore utilizzo di risorse di sistema.

Il funzionamento dei due meccanismi è descritto in dettaglio nelle pubblicazioni Design of a Deadlock-free Train Scheduler: a Model Checking Approach e Measuring and Improving the Completeness of Natural Language Requirements