by Alessandro Fantechi, Francesco Flammini and Stefania Gnesi
The ERCIM Working Group on Formal Methods for Industrial Critical Systems (FMICS), organised a track at the 5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA’12), held in Crete on 15-18 October 2012, to address the application of formal methods to model and analyze complex systems in the context of Intelligent Transportation Systems.
The term “Intelligent Transportation Systems” (ITS) refers to Information and Communication Technology as applied to transport infrastructure and vehicles with the aim of improving transport outcomes such as transport safety, transport productivity, travel reliability, informed travel choices, social equity, environmental performance and network operation resilience. ITS is becoming increasingly important as novel driverless/pilotless applications are emerging.
Based on discussions held by the ERCIM Working Group on Formal Methods for Industrial Critical Systems (FMICS), a track was organized for the ISOLA’12 Conference to address the application of formal methods to model and analyse complex systems in the context of ITS. In fact, modelling and analysis activities are very important to optimize system life-cycle in the design, development, verification and operational stages, and they are essential whenever assessment and certification is required by international standards.
The contributions to the theme “Formal Methods for Intelligent Transportation Systems” addressed three distinct aspects. The first was a general perspective on the introduction of formal methods in the development process of safety-critical systems focusing on model-driven verification techniques, both for functional and non-functional system properties. In particular, the expected impact of a novel software development guideline for safety-critical systems (namely, the avionic DO178-C standard) was evaluated. For the first time, that standard specifically includes formal methods as one of the preferred development and verification techniques.
The other contributions related to two categories of systems in the railway domain, which, owing to their complexity, pose several challenges to current software and system development techniques. The first category addresses driverless metros that integrate several subsystems within complex architectures, which are geographically distributed, featuring strict dependability requirements. The second category is represented by railway interlocking systems: here the complexity lies in the geographical layout of the tracks, points and signals that can be found in stations or in railway yards. Within this context, a particularly challenging problem for current model-checking technology is to automatically verify that interlocking logics designed by railway engineers actually satisfy safety properties (eg, two trains will never be assigned conflicting routes) for medium to large stations.
The lively discussion that took place during the workshop on railway interlocking systems touched on topics such as:
- possible ad hoc optimisations for symbolic model-checking, by means of specific re-orderings of BDD (Binary Decision Diagrams) variables;
- logical and physical distribution of the interlocking control logics;
- the increasing complexity due to the integration and interface of interlocking systems with other signalling systems;
- verification of legacy relay-based interlocking systems which are strictly related to the topology of the controlled layout.
We believe that, despite the limited space available in the program of the track, the contributions succeeded in giving a good overview of the state-of-the-art and of the hard-to-solve open issues, as well as proposing significant directions for the future research in this field.
Link: http://www.cs.uni-potsdam.de/isola/isola2012/
Please contact:
Alessandro Fantechi, Università di Firenze, Italy
E-mail:
Francesco Flammini, Ansaldo STS, Italy
E-mail:
Stefania Gnesi, ISTI–CNR, Italy
E-mail:
