Document - Spatial Model Checking for Smart Stations: Research Challenges

2021

Conference article Open Access

Spatial Model Checking for Smart Stations: Research Challenges

Ter Beek M. H., Ciancia V., Latella D., Massink M., Spagnolo G. O.

Smart stations Spatial logics Spatial model checking Spatio-temporal model checking

In this position paper, we discuss the introduction of spatial verification techniques in an application scenario from smart stations, viz. analysing the user experience with respect to the lighting conditions of station areas. This is a case study in industrial projects. We discuss three challenging use cases for the application of spatial model checking in this setting. First, we envision how to use the spatial model checker VoxLogicA, which can analyse both 2D and 3D voxel-based maps, to explore the areas that users can visit in a station area and to characterise them with respect to their illumination conditions. This is aimed at monitoring a smart station. We also ideate statistical spatio-temporal model checking of the design of energy-saving protocols, exploiting the modelling of user preferences. Finally, we discuss the idea of quantifying the impact of design changes, based on the logs of smart stations, to identify and measure the incidence of undesired events (e.g. non-illuminated platforms where a train is passing by) before and after each change.

Source: FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 39–47, Online conference, 24-26/08/2021

Metrics

Back to previous page

Cite as

BibTeX entry

@inproceedings{oai:it.cnr:prodotti:455997,
	title = {Spatial Model Checking for Smart Stations: Research Challenges},
	author = {Ter Beek M. H. and Ciancia V. and Latella D. and Massink M. and Spagnolo G. O.},
	doi = {10.1007/978-3-030-85248-1_3},
	booktitle = {FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 39–47, Online conference, 24-26/08/2021},
	year = {2021}
}