Contributo in atti di convegno, 2021, ENG, 10.1007/978-3-030-85248-1_3

Spatial Model Checking for Smart Stations: Research Challenges

ter Beek M.H.; Ciancia V.; Latella D.; Massink M.; Spagnolo G.O.

CNR-ISTI, Pisa, Italy; CNR-ISTI, Pisa, Italy; CNR-ISTI, Pisa, Italy; CNR-ISTI, Pisa, Italy; CNR-ISTI, Pisa, Italy

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.

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

Keywords

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

CNR authors

Massink Mieke, Ter Beek Maurice Henri, Latella Diego, Ciancia Vincenzo, Spagnolo Giorgio Oronzo

CNR institutes

ISTI – Istituto di scienza e tecnologie dell'informazione "Alessandro Faedo"

ID: 455997

Year: 2021

Type: Contributo in atti di convegno

Creation: 2021-08-24 10:26:32.000

Last update: 2022-12-01 11:04:36.000

External IDs

CNR OAI-PMH: oai:it.cnr:prodotti:455997

DOI: 10.1007/978-3-030-85248-1_3

Scopus: 2-s2.0-85115174104

ISI Web of Science (WOS): 000884726300003