by Franco Mazzanti, Alessio Ferrari and Giorgio O. Spagnolo (ISTI-CNR)
Autonomous vehicles will become pervasive in the near future. The TRACE-IT project is investigating how gridlocks may be avoided.
One of the pillars of current industry-related research in Europe is the development of intelligent transport systems, which can ease the safe movement of people and goods by means of smart computer platforms that require limited human support. In near future, fleets of autonomous vehicles will need to be supervised and managed. To this end, at ISTI-CNR, we have been developing an advanced automatic train supervision (ATS) system that is able to dispatch trains in a railway layout, while avoiding gridlocks [1]. A gridlock is a localised deadlock in which vehicles mutually block each other in a specific region, while other vehicles are still free to move. While safety is ensured by interlocking systems, efficient dispatching is currently performed by humans, and the TRACE-IT project lays a possible basis for automating this task.
Model-checking technology underpins our approach, which is composed of two main phases: a configuration phase and an actual dispatching phase. In the first phase, model checking is used to identify a set of constraints that the ATS should consider when dispatching the trains to avoid gridlocks. To identify these constraints, the model-checking algorithm initially takes as input a formal model that includes the railway layout, and the planned missions of the train. Then, it explores all the possible sequences of movements of the trains, and identifies potential gridlocks. For each gridlock found, the algorithm produces the critical regions of the layout in which the gridlock might occur, and the maximum number of trains allowed in each region that guarantees the absence of gridlock. These are the constraints that are used by the ATS during the actual dispatching phase. In this phase, before allowing a train to enter one of the constrained critical regions, the ATS checks that the maximum number of trains allowed in that region is not exceeded. When novel missions or vehicles enter into play, a reconfiguration cycle is performed through model checking, following the first phase. Hence, new regions and numerical constraints are produced for consideration by the ATS.
In TRACE-IT, the approach was experimented on a realistic layout for metro systems provided by ECM S.p.A., and reported in Figure 1. The figure depicts the physical layout in black solid lines, and the missions of eight trains in coloured lines. Within TRACE-IT, configuration and reconfiguration were performed offline by means of the general-purpose model checker UMC, belonging to the KandISTI family [2]. We have also experimented the implementation of a dynamic reconfiguration process, by developing a special-purpose model checker – integrated within the ATS – which focusses on the verification of these particular properties for this particular class of models.
Figure 1: Metro layout for TRACE-IT project.
This gridlock avoidance approach can be adapted to any kind of vehicle moving along pre-defined paths – either physical or virtual – that should satisfy safety distance requirements. The fleets of autonomous vehicles that can be managed with this approach range from cars to trucks, and from drones to swarms of robots. Of course, when the layout of movements is particularly large, it may become necessary to decompose it into smaller fragments to avoid exponential state-space explosion during the analysis [3].
This work was carried out within the PAR FAS 2007-2013 TRACE-IT Project, funded by the Tuscan Region, and involving the University of Florence, and railway signalling manufacturer ECM S.p.A.
Link:
http://fmt.isti.cnr.it/umc
References:
[1] F. Mazzanti, G.O. Spagnolo, S. Della Longa, A. Ferrari: "Deadlock avoidance in train scheduling: A model checking approach". FMICS 2014, LNCS Vol. 8718, Springer, 2014, 109-123.
[2] M.H. ter Beek, S. Gnesi, F. Mazzanti: "From EU projects to a family of model checkers". Software, Services, and Systems, LNCS Vol. 8950, Springer, 2015, pp. 312-328.
[3] A. Ferrari, G. Magnani, D. Grasso, A. Fantechi: "Model checking interlocking control tables". FORMS/FORMAT 2010. Springer, 2011, pp. 107-115.
Please contact:
Franco Mazzanti, ISTI-CNR, Italy
